[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.

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5d3115d8d7..b0f6301192 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,7 +30,7 @@ open Common
 let toplevel_env () =
   let get_reference = function
     | (_,kn), Lib.Leaf o ->
-	let mp,_,l = KerName.repr kn in
+        let mp,l = KerName.repr kn in
 	begin match Libobject.object_tag o with
 	  | "CONSTANT" ->
             let constant = Global.lookup_constant (Constant.make1 kn) in
@@ -124,7 +124,7 @@ module Visit : VISIT = struct
 end
 
 let add_field_label mp = function
-  | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab)
+  | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make mp lab)
   | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
 
 let rec add_labels mp = function
@@ -208,10 +208,10 @@ let env_for_mtb_with_def env mp me reso idl =
   Modops.add_structure mp before reso env
 
 let make_cst resolver mp l =
-  Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
+  Mod_subst.constant_of_delta_kn resolver (KerName.make mp l)
 
 let make_mind resolver mp l =
-  Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l)
+  Mod_subst.mind_of_delta_kn resolver (KerName.make mp l)
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)