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

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 03fee1ab51..93d5f8bfa2 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -70,12 +70,12 @@ let solve_delta_kn resolve kn =
       | Equiv kn1 -> kn1
       | Inline _ -> raise Not_found
   with Not_found ->
-    let mp,dir,l = KerName.repr kn in
+    let mp,l = KerName.repr kn in
     let new_mp = find_prefix resolve mp in
     if mp == new_mp then
       kn
     else
-      KerName.make new_mp dir l
+      KerName.make new_mp l
 
 let gen_of_delta resolve x kn fix_can =
   let new_kn = solve_delta_kn resolve kn in
@@ -129,17 +129,17 @@ let subst_mp sub mp =
   | Some (mp',_) -> mp'
 
 let subst_kn_delta sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',resolve) ->
-      solve_delta_kn resolve (KerName.make mp' dir l)
+      solve_delta_kn resolve (KerName.make mp' l)
    | None -> kn
 
 let subst_kn sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      KerName.make mp' dir l
+      KerName.make mp' l
    | None -> kn
 
 exception No_subst
@@ -156,16 +156,16 @@ let gen_subst_mp f sub mp1 mp2 =
     | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
     | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
 
-let make_mind_equiv mpu mpc dir l =
-  let knu = KerName.make mpu dir l in
+let make_mind_equiv mpu mpc l =
+  let knu = KerName.make mpu l in
   if mpu == mpc then MutInd.make1 knu
-  else MutInd.make knu (KerName.make mpc dir l)
+  else MutInd.make knu (KerName.make mpc l)
 
 let subst_ind sub mind =
   let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in
-  let mp1,dir,l = KerName.repr kn1 in
-  let mp2,_,_ = KerName.repr kn2 in
-  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+  let mp1,l = KerName.repr kn1 in
+  let mp2,_ = KerName.repr kn2 in
+  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 l in
   try
     let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
     match side with
@@ -173,16 +173,16 @@ let subst_ind sub mind =
       | Canonical -> mind_of_delta2 resolve mind'
   with No_subst -> mind
 
-let make_con_equiv mpu mpc dir l =
-  let knu = KerName.make mpu dir l in
+let make_con_equiv mpu mpc l =
+  let knu = KerName.make mpu l in
   if mpu == mpc then Constant.make1 knu
-  else Constant.make knu (KerName.make mpc dir l)
+  else Constant.make knu (KerName.make mpc l)
 
 let subst_con0 sub con u =
   let kn1,kn2 = Constant.user con, Constant.canonical con in
-  let mp1,dir,l = KerName.repr kn1 in
-  let mp2,_,_ = KerName.repr kn2 in
-  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
+  let mp1,l = KerName.repr kn1 in
+  let mp2,_ = KerName.repr kn2 in
+  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 l in
   let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
   match constant_of_delta_with_inline resolve con' with
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 1fd86bc368..0478765a81 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -34,7 +34,7 @@ let string_of_mp mp =
   if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
 
 let prkn kn =
-  let (mp,_,l) = KerName.repr kn in
+  let (mp,l) = KerName.repr kn in
   str(string_of_mp mp ^ "." ^ Label.to_string l)
 let prcon c =
   let ck = Constant.canonical c in
diff --git a/checker/modops.ml b/checker/modops.ml
index b92d7bbf1f..541d009ff9 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -55,7 +55,7 @@ let module_body_of_type mp mtb =
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
-    let kn = KerName.make2 mp l in
+    let kn = KerName.make mp l in
     let con = Constant.make1 kn in
     let mind = mind_of_delta resolver (MutInd.make1 kn) in
       match elem with
diff --git a/checker/values.ml b/checker/values.ml
index 35027d5bfb..24f10b7a87 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -98,7 +98,7 @@ let rec v_mp = Sum("module_path",0,
   [|[|v_dp|];
     [|v_uid|];
     [|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;v_id;Int|]
 let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
 let v_ind = v_tuple "inductive" [|v_cst;Int|]
 let v_cons = v_tuple "constructor" [|v_ind;Int|]