[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, 14 insertions, 15 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index d413cd1e6d..bdeb6fca60 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -588,7 +588,7 @@ let pp_global k r =
   let ls = ref_renaming (k,r) in
   assert (List.length ls > 1);
   let s = List.hd ls in
-  let mp,_,l = repr_of_r r in
+  let mp,l = repr_of_r r in
   if ModPath.equal mp (top_visible_mp ()) then
     (* simpliest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
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. *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6ee1770a4e..7b4fd280bd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -36,16 +36,16 @@ let occur_kn_in_ref kn = function
   | ConstRef _ | VarRef _ -> false
 
 let repr_of_r = function
-  | ConstRef kn -> Constant.repr3 kn
+  | ConstRef kn -> Constant.repr2 kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
+  | ConstructRef ((kn,_),_) -> MutInd.repr2 kn
   | VarRef v -> KerName.repr (Lib.make_kn v)
 
 let modpath_of_r r =
-  let mp,_,_ = repr_of_r r in mp
+  let mp,_ = repr_of_r r in mp
 
 let label_of_r r =
-  let _,_,l = repr_of_r r in l
+  let _,l = repr_of_r r in l
 
 let rec base_mp = function
   | MPdot (mp,l) -> base_mp mp
@@ -95,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
 
 let labels_of_ref r =
   let mp_top = Lib.current_mp () in
-  let mp,_,l = repr_of_r r in
+  let mp,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
 
@@ -189,7 +189,7 @@ let init_recursors () = recursors := KNset.empty
 let add_recursors env ind =
   let kn = MutInd.canonical ind in
   let mk_kn id =
-    KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id)
+    KerName.make (KerName.modpath kn) (Label.of_id id)
   in
   let mib = Environ.lookup_mind ind env in
   Array.iter
@@ -287,7 +287,7 @@ let safe_pr_long_global r =
   try Printer.pr_global r
   with Not_found -> match r with
     | ConstRef kn ->
-	let mp,_,l = Constant.repr3 kn in
+        let mp,l = Constant.repr2 kn in
 	str ((ModPath.to_string mp)^"."^(Label.to_string l))
     | _ -> assert false
 
@@ -653,8 +653,7 @@ let inline_extraction : bool * GlobRef.t list -> obj =
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        classify_function = (fun o -> Substitute o);
-       discharge_function =
-	(fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
+       discharge_function = (fun (_,x) -> Some x);
        subst_function =
         (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a8baeaf1b6..acc1bfee8a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
 (*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
 
 val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
-val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t
+val repr_of_r : GlobRef.t -> ModPath.t * Label.t
 val modpath_of_r : GlobRef.t -> ModPath.t
 val label_of_r : GlobRef.t -> Label.t
 val base_mp : ModPath.t -> ModPath.t