[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, 6 insertions, 8 deletions

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) =