Clean-up around substitution of globals

interp/impargs.ml

@@ -535,7 +535,7 @@ let cache_implicits o =
   load_implicits 1 o
 
 let subst_implicits_decl subst (r,imps as o) =
-  let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
+  let r' = subst_global_reference subst r in if r==r' then o else (r',imps)
 
 let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)

interp/notation.ml

@@ -1285,7 +1285,7 @@ let subst_scope_class subst cs =
   try Some (subst_cl_typ subst cs) with Not_found -> None
 
 let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
-  let r' = fst (subst_global subst r) in
+  let r' = subst_global_reference subst r in
   let subst_cl ocl = match ocl with
     | None -> ocl
     | Some cl ->

interp/notation_ops.ml

@@ -625,7 +625,7 @@ let rec subst_notation_constr subst bound raw =
   | NHole (knd, naming, solve) ->
     let nknd = match knd with
     | Evar_kinds.ImplicitArg (ref, i, b) ->
-      let nref, _ = subst_global subst ref in
+      let nref = subst_global_reference subst ref in
       if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
     | _ -> knd
     in

kernel/mod_subst.ml

@@ -316,9 +316,6 @@ let subst_con sub cst =
   try subst_con0 sub cst
   with No_subst -> fst cst, mkConstU cst
 
-let subst_con_kn sub con =
-  subst_con sub (con,Univ.Instance.empty)
-
 let subst_pcon sub (_con,u as pcon) =
   try let con', _can = subst_con0 sub pcon in
 	con',u
@@ -329,9 +326,19 @@ let subst_pcon_term sub (_con,u as pcon) =
 	(con',u), can
   with No_subst -> pcon, mkConstU pcon
 
-let subst_constant sub con =
-  try fst (subst_con0 sub (con,Univ.Instance.empty))
-  with No_subst -> con
+let subst_constant sub cst =
+  try
+    let mpu,l = Constant.repr2 cst in
+    let mpc = KerName.modpath (Constant.canonical cst) in
+    let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
+    let knu = KerName.make mpu l in
+    let knc = if mpu == mpc then knu else KerName.make mpc l in
+    let knc' =
+      progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
+    in
+    let cst' = Constant.make knu knc' in
+    cst'
+  with No_subst -> cst
 
 let subst_proj_repr sub p =
   Projection.Repr.map (subst_mind sub) p

kernel/mod_subst.mli

@@ -141,9 +141,6 @@ val subst_pcon :
 val subst_pcon_term :
   substitution -> pconstant -> pconstant * constr
 
-val subst_con_kn :
-  substitution -> Constant.t -> Constant.t * constr
-
 val subst_constant :
   substitution -> Constant.t -> Constant.t
 

library/globnames.ml

@@ -29,6 +29,11 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
+let subst_constructor_reference subst (ind,j as ref) =
+  let ind' = subst_ind subst ind in
+    if ind==ind' then ref
+    else (ind',j)
+
 let subst_constructor subst (ind,j as ref) =
   let ind' = subst_ind subst ind in
     if ind==ind' then ref, mkConstruct ref
@@ -43,13 +48,13 @@ let subst_global_reference subst ref = match ref with
     let ind' = subst_ind subst ind in
       if ind==ind' then ref else IndRef ind'
   | ConstructRef ((kn,i),j as c) ->
-    let c',t = subst_constructor subst c in
+    let c' = subst_constructor_reference subst c in
       if c'==c then ref else ConstructRef c'
 
 let subst_global subst ref = match ref with
   | VarRef var -> ref, mkVar var
   | ConstRef kn ->
-     let kn',t = subst_con_kn subst kn in
+     let kn',t = subst_con subst (Univ.in_punivs kn) in
       if kn==kn' then ref, mkConst kn else ConstRef kn', t
   | IndRef ind ->
       let ind' = subst_ind subst ind in

library/globnames.mli

@@ -37,6 +37,9 @@ val destConstructRef : GlobRef.t -> constructor
 val is_global : GlobRef.t -> constr -> bool
 
 val subst_constructor : substitution -> constructor -> constructor * constr
+[@@ocaml.deprecated "Use subst_constructor_reference"]
+
+val subst_constructor_reference : substitution -> constructor -> constructor
 val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 

plugins/extraction/table.ml

@@ -655,7 +655,7 @@ let inline_extraction : bool * GlobRef.t list -> obj =
        classify_function = (fun o -> Substitute o);
        discharge_function = (fun (_,x) -> Some x);
        subst_function =
-        (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
+        (fun (s,(b,l)) -> (b,(List.map (fun x -> subst_global_reference s x) l)))
     }
 
 (* Grammar entries. *)
@@ -736,7 +736,7 @@ let implicit_extraction : GlobRef.t * int_or_id list -> obj =
        cache_function = (fun (_,(r,l)) -> add_implicits r l);
        load_function = (fun _ (_,(r,l)) -> add_implicits r l);
        classify_function = (fun o -> Substitute o);
-       subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
+       subst_function = (fun (s,(r,l)) -> (subst_global_reference s r, l))
     }
 
 (* Grammar entries. *)
@@ -858,7 +858,7 @@ let in_customs : GlobRef.t * string list * string -> obj =
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
        classify_function = (fun o -> Substitute o);
        subst_function =
-        (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
+        (fun (s,(r,ids,str)) -> (subst_global_reference s r, ids, str))
     }
 
 let in_custom_matchs : GlobRef.t * string -> obj =
@@ -867,7 +867,7 @@ let in_custom_matchs : GlobRef.t * string -> obj =
        cache_function = (fun (_,(r,s)) -> add_custom_match r s);
        load_function = (fun _ (_,(r,s)) -> add_custom_match r s);
        classify_function = (fun o -> Substitute o);
-       subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
+       subst_function = (fun (subs,(r,s)) -> (subst_global_reference subs r, s))
     }
 
 (* Grammar entries. *)

pretyping/arguments_renaming.ml

@@ -37,9 +37,9 @@ let classify_rename_args = function
   | ReqLocal, _ -> Dispose
   | ReqGlobal _, _ as o -> Substitute o
 
-let subst_rename_args (subst, (_, (r, names as orig))) = 
+let subst_rename_args (subst, (_, (r, names as orig))) =
   ReqLocal,
-  let r' = fst (subst_global subst r) in 
+  let r' = subst_global_reference subst r in
   if r==r' then orig else (r', names)
 
 let discharge_rename_args = function

pretyping/classops.ml

@@ -192,7 +192,7 @@ let subst_cl_typ subst ct = match ct with
     let c' = subst_proj_repr subst c in
       if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
-      let c',t = subst_con_kn subst c in
+      let c',t = subst_con subst (Univ.in_punivs c) in
 	if c' == c then ct else
          pi1 (find_class_type Evd.empty (EConstr.of_constr t))
   | CL_IND i ->

pretyping/detyping.ml

@@ -1021,7 +1021,7 @@ let rec subst_glob_constr subst = DAst.map (function
   | GHole (knd, naming, solve) as raw ->
     let nknd = match knd with
     | Evar_kinds.ImplicitArg (ref, i, b) ->
-      let nref, _ = subst_global subst ref in
+      let nref = subst_global_reference subst ref in
       if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
     | _ -> knd
     in

pretyping/heads.ml

@@ -156,7 +156,7 @@ let cache_head o =
 
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
-      let cst,c = subst_con_kn subst cst in
+      let cst,c = subst_con subst (Univ.in_punivs cst) in
       if isConst c && Constant.equal (fst (destConst c)) cst then
         (* A change of the prefix of the constant *)
         k

pretyping/recordops.ml

@@ -71,10 +71,10 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    List.Smart.map
-     (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn)))
+     (Option.Smart.map (subst_constant subst))
     projs
   in
-  let id' = fst (subst_constructor subst id) in
+  let id' = subst_constructor_reference subst id in
     if projs' == projs && kn' == kn && id' == id then obj else
       ((kn',i),id',kl,projs')
 

pretyping/reductionops.ml

@@ -116,7 +116,7 @@ module ReductionBehaviour = struct
 
   let subst (subst, (_, (r,o as orig))) =
     ReqLocal,
-    let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
+    let r' = subst_global_reference subst r in if r==r' then orig else (r',o)
 
   let discharge = function
     | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->

pretyping/typeclasses.ml

@@ -193,7 +193,7 @@ let cache_class = load_class
 let subst_class (subst,cl) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst c = Mod_subst.subst_mps subst c
-  and do_subst_gr gr = fst (subst_global subst gr) in
+  and do_subst_gr gr = subst_global_reference subst gr in
   let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
     List.Smart.map (Option.Smart.map do_subst_gr) grs,
@@ -369,8 +369,8 @@ let cache_instance (_, (action, i)) =
 
 let subst_instance (subst, (action, inst)) = action,
   { inst with 
-      is_class = fst (subst_global subst inst.is_class);
-      is_impl = fst (subst_global subst inst.is_impl) }
+      is_class = subst_global_reference subst inst.is_class;
+      is_impl = subst_global_reference subst inst.is_impl }
 
 let discharge_instance (_, (action, inst)) =
   match inst.is_global with

tactics/hints.ml

@@ -471,7 +471,7 @@ let subst_path_atom subst p =
   match p with
   | PathAny -> p
   | PathHints grs ->
-    let gr' gr = fst (subst_global subst gr) in
+    let gr' gr = subst_global_reference subst gr in
     let grs' = List.Smart.map gr' grs in
       if grs' == grs then p else PathHints grs'
 

tactics/term_dnet.ml

@@ -337,7 +337,7 @@ struct
   let subst s t =
     let sleaf id = Ident.subst s id in
     let snode = function
-      | DTerm.DRef gr -> DTerm.DRef (fst (subst_global s gr))
+      | DTerm.DRef gr -> DTerm.DRef (subst_global_reference s gr)
       | n -> n in
     TDnet.map sleaf snode t