Merge PR #8555: Remove section paths from kernel names

7 files changed, 24 insertions, 42 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index b8958ca944..3da1ab7439 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -46,10 +46,9 @@ let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
      (try 
        let vars = Lib.variable_section_segment_of_reference c in
-       let c' = pop_global_reference c in
        let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
-       Some (ReqGlobal (c', names), (c', names'))
+       Some (ReqGlobal (c, names), (c, names'))
      with Not_found -> Some req)
   | _ -> None
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b264e31474..b026397abf 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -451,12 +451,6 @@ let subst_coercion (subst, c) =
   else { c with coercion_type = coe; coercion_source = cls;
                 coercion_target = clt; coercion_is_proj = clp; }
 
-let discharge_cl = function
-  | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
-  | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
-  | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p)
-  | cl -> cl
-
 let discharge_coercion (_, c) =
   if c.coercion_local then None
   else
@@ -467,9 +461,6 @@ let discharge_coercion (_, c) =
       with Not_found -> 0
     in
     let nc = { c with
-      coercion_type = Lib.discharge_global c.coercion_type;
-      coercion_source = discharge_cl c.coercion_source;
-      coercion_target = discharge_cl c.coercion_target;
       coercion_params = n + c.coercion_params;
       coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
     } in
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 7d9debce34..a3e4eb8971 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -14,7 +14,6 @@ open Constr
 open Vars
 open Mod_subst
 open Environ
-open Globnames
 open Libobject
 open Lib
 open Context.Named.Declaration
@@ -171,7 +170,7 @@ let subst_head (subst,(ref,k)) =
 
 let discharge_head (_,(ref,k)) =
   match ref with
-  | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
+  | EvalConstRef cst -> Some (ref, k)
   | EvalVarRef id -> None
 
 let rebuild_head (ref,k) =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 418fdf2a26..4ee7e667fe 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -601,13 +601,13 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = KerName.repr (MutInd.canonical kn) in
+  let mp,l = KerName.repr (MutInd.canonical kn) in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in
+    let cst =Global.constant_of_delta_kn (KerName.make mp (Label.of_id id)) in
     let _ = Global.lookup_constant cst in
       ConstRef cst
   with Not_found ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c25416405e..3719f9302a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -79,12 +79,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
     if projs' == projs && kn' == kn && id' == id then obj else
       ((kn',i),id',kl,projs')
 
-let discharge_constructor (ind, n) =
-  (Lib.discharge_inductive ind, n)
-
-let discharge_structure (_,(ind,id,kl,projs)) =
-  Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
-        List.map (Option.map Lib.discharge_con) projs)
+let discharge_structure (_,x) = Some x
 
 let inStruc : struc_tuple -> obj =
   declare_object {(default_object "STRUCTURE") with
@@ -319,8 +314,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
   let ind' = subst_ind subst ind in
   if cst' == cst && ind' == ind then obj else (cst',ind')
 
-let discharge_canonical_structure (_,(cst,ind)) =
-  Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
+let discharge_canonical_structure (_,x) = Some x
 
 let inCanonStruc : Constant.t * inductive -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e8c3b3e2b3..5dbe95a471 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -132,8 +132,7 @@ module ReductionBehaviour = struct
           { b with b_nargs = nargs'; b_recargs = recargs' }
         else b
       in
-      let c = Lib.discharge_con c in
-      Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
+      Some (ReqGlobal (gr, req), (ConstRef c, b))
     | _ -> None
 
   let rebuild = function
@@ -713,8 +712,8 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Name id ->
     let open UnivProblem in
     try
-      let (cst_mod,cst_sect,_) = Constant.repr3 reference in
-      let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
+      let (cst_mod,_) = Constant.repr2 reference in
+      let cst = Constant.make2 cst_mod (Label.of_id id) in
       let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 67c5643459..7e5815acd1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -222,26 +222,26 @@ let discharge_class (_,cl) =
                              | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.Smart.map (Option.Smart.map Lib.discharge_global) grs
-      @ newgrs
+      grs @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
-  let cl_impl' = Lib.discharge_global cl.cl_impl in
-  if cl_impl' == cl.cl_impl then cl else
+  try
     let info = abs_context cl in
     let ctx = info.Lib.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
     let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in
-      { cl_univs = cl_univs';
-        cl_impl = cl_impl';
-	cl_context = context;
-	cl_props = props;
-        cl_projs = List.Smart.map discharge_proj cl.cl_projs;
-	cl_strict = cl.cl_strict;
-	cl_unique = cl.cl_unique
-      }
+    let discharge_proj x = x in
+    { cl_univs = cl_univs';
+      cl_impl = cl.cl_impl;
+      cl_context = context;
+      cl_props = props;
+      cl_projs = List.Smart.map discharge_proj cl.cl_projs;
+      cl_strict = cl.cl_strict;
+      cl_unique = cl.cl_unique
+    }
+  with Not_found -> (* not defined in the current section *)
+    cl
 
 let rebuild_class cl = 
   try 
@@ -365,8 +365,8 @@ let discharge_instance (_, (action, inst)) =
     Some (action,
     { inst with 
       is_global = Some (pred n);
-      is_class = Lib.discharge_global inst.is_class;
-      is_impl = Lib.discharge_global inst.is_impl })
+      is_class = inst.is_class;
+      is_impl = inst.is_impl })
     
 
 let is_local i = (i.is_global == None)