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

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)