[kernel] Remove section paths from `KerName.t`

We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.

Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.

4 files changed, 11 insertions, 15 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 23c68b5e18..f4e57073cc 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -78,7 +78,6 @@ let check_exists sp =
 
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
-  let _,dir,_ = KerName.repr kn in
   let kn' =
     match obj.cst_decl with
     | None ->
@@ -87,7 +86,7 @@ let cache_constant ((sp,kn), obj) =
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     | Some decl ->
       let () = check_exists sp in
-      Global.add_constant dir id decl
+      Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -136,7 +135,7 @@ let register_side_effect (c, role) =
     cst_kind = IsProof Theorem;
     cst_locl = false;
   } in
-  let id = Label.to_id (pi3 (Constant.repr3 c)) in
+  let id = Label.to_id (Constant.label c) in
   ignore(add_leaf id o);
   update_tables c;
   match role with
@@ -311,8 +310,7 @@ let cache_inductive ((sp,kn),mie) =
   let names = inductive_names sp kn mie in
   List.iter check_exists (List.map fst names);
   let id = basename sp in
-  let _,dir,_ = KerName.repr kn in
-  let kn' = Global.add_mind dir id mie in
+  let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
   add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index ccad6b19eb..f5be0ddbae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -234,7 +234,7 @@ let add_glob ?loc ref =
     add_glob_gen ?loc sp lib_dp ty
 
 let mp_of_kn kn =
-  let mp,sec,l = Names.KerName.repr kn in
+  let mp,l = Names.KerName.repr kn in
     Names.MPdot (mp,l)
 
 let add_glob_kn ?loc kn =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 3603367cf1..ce33cb8731 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -561,29 +561,27 @@ let discharge_implicits (_,(req,l)) =
   | ImplInteractive (ref,flags,exp) ->
     (try
       let vars = variable_section_segment_of_reference ref in
-      let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
-      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
-      Some (ImplInteractive (ref',flags,exp),l')
+      let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      Some (ImplInteractive (ref,flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
     (try
-      let con' = pop_con con in
       let vars = variable_section_segment_of_reference (ConstRef con) in
       let extra_impls = impls_of_context vars in
       let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
-      let l' = [ConstRef con',newimpls] in
-	Some (ImplConstant (con',flags),l')
+      let l' = [ConstRef con,newimpls] in
+        Some (ImplConstant (con,flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
 	let vars = variable_section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
-	((if isVarRef gr then gr else pop_global_reference gr),
+        (gr,
 	 List.map (add_section_impls vars extra_impls) l)) l
       in
-	Some (ImplMutualInductive (pop_kn kn,flags),l')
+        Some (ImplMutualInductive (kn,flags),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
 
 let rebuild_implicits (req,l) =
diff --git a/interp/notation.ml b/interp/notation.ml
index 02c7812e21..6104ab16c7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1304,7 +1304,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
         vars |> List.map fst |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
-    Some (req,Lib.discharge_global r,n,l,[])
+    Some (req,r,n,l,[])
 
 let classify_arguments_scope (req,_,_,_,_ as obj) =
   if req == ArgsScopeNoDischarge then Dispose else Substitute obj