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

12 files changed, 80 insertions, 116 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b361e36bbf..b39aed01e8 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -15,7 +15,6 @@
 (* This module implements kernel-level discharching of local
    declarations over global constants and inductive types *)
 
-open CErrors
 open Util
 open Names
 open Term
@@ -28,18 +27,6 @@ module RelDecl = Context.Rel.Declaration
 
 (*s Cooking the constants. *)
 
-let pop_dirpath p = match DirPath.repr p with
-  | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.")
-  | _::l -> DirPath.make l
-
-let pop_mind kn =
-  let (mp,dir,l) = MutInd.repr3 kn in
-  MutInd.make3 mp (pop_dirpath dir) l
-
-let pop_con con =
-  let (mp,dir,l) = Constant.repr3 con in
-  Constant.make3 mp (pop_dirpath dir) l
-
 type my_global_reference =
   | ConstRef of Constant.t
   | IndRef of inductive
@@ -71,29 +58,26 @@ let instantiate_my_gr gr u =
 let share cache r (cstl,knl) =
   try RefTable.find cache r
   with Not_found ->
-  let f,(u,l) =
+  let (u,l) =
     match r with
-    | IndRef (kn,i) ->
-	IndRef (pop_mind kn,i), Mindmap.find kn knl
-    | ConstructRef ((kn,i),j) ->
-	ConstructRef ((pop_mind kn,i),j), Mindmap.find kn knl
+    | IndRef (kn,_i) ->
+        Mindmap.find kn knl
+    | ConstructRef ((kn,_i),_j) ->
+        Mindmap.find kn knl
     | ConstRef cst ->
-	ConstRef (pop_con cst), Cmap.find cst cstl in
-  let c = (f, (u, Array.map mkVar l)) in
+        Cmap.find cst cstl in
+  let c = (u, Array.map mkVar l) in
   RefTable.add cache r c;
   c
 
 let share_univs cache r u l =
-  let r', (u', args) = share cache r l in
-    mkApp (instantiate_my_gr r' (Instance.append u' u), args)
+  let (u', args) = share cache r l in
+    mkApp (instantiate_my_gr r (Instance.append u' u), args)
 
 let update_case_info cache ci modlist =
   try
-    let ind, n =
-      match share cache (IndRef ci.ci_ind) modlist with
-      | (IndRef f,(_u,l)) -> (f, Array.length l)
-      | _ -> assert false in
-    { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
+    let (_u,l) = share cache (IndRef ci.ci_ind) modlist in
+    { ci with ci_npar = ci.ci_npar + Array.length l }
   with Not_found ->
     ci
 
@@ -129,7 +113,7 @@ let expmod_constr cache modlist c =
       | Proj (p, c') ->
         let map cst npars =
           let _, newpars = Mindmap.find cst (snd modlist) in
-          pop_mind cst, npars + Array.length newpars
+          (cst, npars + Array.length newpars)
         in
         let p' = try Projection.map_npars map p with Not_found -> p in
         let c'' = substrec c' in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index bff3092655..2a91c7dab0 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -173,12 +173,12 @@ let solve_delta_kn resolve kn =
       | Inline (lev, Some c) ->	raise (Change_equiv_to_inline (lev,c))
       | Inline (_, None) -> 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 kn_of_delta resolve kn =
   try solve_delta_kn resolve kn
@@ -245,18 +245,18 @@ 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
@@ -275,12 +275,12 @@ let progress f x ~orelse =
   if y != x then y else orelse
 
 let subst_mind sub mind =
-  let mpu,dir,l = MutInd.repr3 mind in
+  let mpu,l = MutInd.repr2 mind in
   let mpc = KerName.modpath (MutInd.canonical mind) in
   try
     let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
-    let knu = KerName.make mpu dir l in
-    let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+    let knu = KerName.make mpu l in
+    let knc = if mpu == mpc then knu else KerName.make mpc l in
     let knc' =
       progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
     in
@@ -295,11 +295,11 @@ let subst_pind sub (ind,u) =
   (subst_ind sub ind, u)
 
 let subst_con0 sub (cst,u) =
-  let mpu,dir,l = Constant.repr3 cst in
+  let mpu,l = Constant.repr2 cst in
   let mpc = KerName.modpath (Constant.canonical cst) in
   let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
-  let knu = KerName.make mpu dir l in
-  let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+  let knu = KerName.make mpu l in
+  let knc = if mpu == mpc then knu else KerName.make mpc l in
   match search_delta_inline resolve knu knc with
     | Some (ctx, t) ->
       (* In case of inlining, discard the canonical part (cf #2608) *)
@@ -433,10 +433,10 @@ let rec replace_mp_in_mp mpfrom mpto mp =
     | _ -> mp
 
 let replace_mp_in_kn mpfrom mpto kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   let mp'' = replace_mp_in_mp mpfrom mpto mp in
     if mp==mp'' then kn
-    else KerName.make mp'' dir l
+    else KerName.make mp'' l
 
 let rec mp_in_mp mp mp1 =
   match mp1 with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 424d329e09..bab2eae3df 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -289,10 +289,10 @@ let add_retroknowledge =
 let rec add_structure mp sign resolver linkinfo env =
   let add_one env (l,elem) = match elem with
     |SFBconst cb ->
-      let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
+      let c = constant_of_delta_kn resolver (KerName.make mp l) in
       Environ.add_constant_key c cb linkinfo env
     |SFBmind mib ->
-      let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+      let mind = mind_of_delta_kn resolver (KerName.make mp l) in
       let mib = 
 	if mib.mind_private != None then 
 	  { mib with mind_private = Some true }
@@ -331,7 +331,7 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
   |Def _ -> cb
   |_ ->
-    let kn = KerName.make2 mp_from l in
+    let kn = KerName.make mp_from l in
     let con = constant_of_delta_kn resolver kn in
     let u =
       match cb.const_universes with
@@ -450,8 +450,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
           (* If we are performing an inclusion we need to add
              the fact that the constant mp_to.l is \Delta-equivalent
              to reso(mp_from.l) *)
-          let kn_from = KerName.make2 mp_from l in
-          let kn_to = KerName.make2 mp_to l in
+          let kn_from = KerName.make mp_from l in
+          let kn_to = KerName.make mp_to l in
           let old_name = kn_of_delta reso kn_from in
 	  add_kn_delta_resolver kn_to old_name reso', str'
 	else
@@ -471,8 +471,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
         in
 	(* Same as constant *)
 	if incl then
-	  let kn_from = KerName.make2 mp_from l in
-	  let kn_to = KerName.make2 mp_to l in
+          let kn_from = KerName.make mp_from l in
+          let kn_to = KerName.make mp_to l in
 	  let old_name = kn_of_delta reso kn_from in
           add_kn_delta_resolver kn_to old_name reso', str'
 	else
diff --git a/kernel/names.ml b/kernel/names.ml
index 6d33f233e9..1e28ec51fb 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -365,7 +365,6 @@ module KerName = struct
 
   type t = {
     modpath : ModPath.t;
-    dirpath : DirPath.t;
     knlabel : Label.t;
     mutable refhash : int;
     (** Lazily computed hash. If unset, it is set to negative values. *)
@@ -373,22 +372,18 @@ module KerName = struct
 
   type kernel_name = t
 
-  let make modpath dirpath knlabel =
-    { modpath; dirpath; knlabel; refhash = -1; }
-  let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
+  let make modpath knlabel =
+    { modpath; knlabel; refhash = -1; }
+  let repr kn = (kn.modpath, kn.knlabel)
 
-  let make2 modpath knlabel =
-    { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
+  let make2 = make
+  [@@ocaml.deprecated "Please use [KerName.make]"]
 
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
   let to_string_gen mp_to_string kn =
-    let dp =
-      if DirPath.is_empty kn.dirpath then "."
-      else "#" ^ DirPath.to_string kn.dirpath ^ "#"
-    in
-    mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+    mp_to_string kn.modpath ^ "." ^ Label.to_string kn.knlabel
 
   let to_string kn = to_string_gen ModPath.to_string kn
 
@@ -402,9 +397,7 @@ module KerName = struct
       let c = String.compare kn1.knlabel kn2.knlabel in
       if not (Int.equal c 0) then c
       else
-        let c = DirPath.compare kn1.dirpath kn2.dirpath in
-        if not (Int.equal c 0) then c
-        else ModPath.compare kn1.modpath kn2.modpath
+        ModPath.compare kn1.modpath kn2.modpath
 
   let equal kn1 kn2 =
     let h1 = kn1.refhash in
@@ -412,7 +405,6 @@ module KerName = struct
     if 0 <= h1 && 0 <= h2 && not (Int.equal h1 h2) then false
     else
       Label.equal kn1.knlabel kn2.knlabel &&
-      DirPath.equal kn1.dirpath kn2.dirpath &&
       ModPath.equal kn1.modpath kn2.modpath
 
   open Hashset.Combine
@@ -420,8 +412,8 @@ module KerName = struct
   let hash kn =
     let h = kn.refhash in
     if h < 0 then
-      let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in
-      let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in
+      let { modpath = mp; knlabel = lbl; _ } = kn in
+      let h = combine (ModPath.hash mp) (Label.hash lbl) in
       (* Ensure positivity on all platforms. *)
       let h = h land 0x3FFFFFFF in
       let () = kn.refhash <- h in
@@ -432,12 +424,11 @@ module KerName = struct
     type t = kernel_name
     type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t)
         * (string -> string)
-    let hashcons (hmod,hdir,hstr) kn =
-      let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
-      { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
+    let hashcons (hmod,_hdir,hstr) kn =
+      let { modpath = mp; knlabel = l; refhash; } = kn in
+      { modpath = hmod mp; knlabel = hstr l; refhash; }
     let eq kn1 kn2 =
-      kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
-        kn1.knlabel == kn2.knlabel
+      kn1.modpath == kn2.modpath && kn1.knlabel == kn2.knlabel
     let hash = hash
   end
 
@@ -492,21 +483,20 @@ module KerPair = struct
   let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
 
   let make1 = same
-  let make2 mp l = same (KerName.make2 mp l)
-  let make3 mp dir l = same (KerName.make mp dir l)
-  let repr3 kp = KerName.repr (user kp)
+  let make2 mp l = same (KerName.make mp l)
+  let repr2 kp = KerName.repr (user kp)
   let label kp = KerName.label (user kp)
   let modpath kp = KerName.modpath (user kp)
 
   let change_label kp lbl =
-    let (mp1,dp1,l1) = KerName.repr (user kp)
-    and (mp2,dp2,l2) = KerName.repr (canonical kp) in
-    assert (String.equal l1 l2 && DirPath.equal dp1 dp2);
+    let (mp1,l1) = KerName.repr (user kp)
+    and (mp2,l2) = KerName.repr (canonical kp) in
+    assert (String.equal l1 l2);
     if String.equal lbl l1 then kp
     else
-      let kn = KerName.make mp1 dp1 lbl in
+      let kn = KerName.make mp1 lbl in
       if mp1 == mp2 then same kn
-      else make kn (KerName.make mp2 dp2 lbl)
+      else make kn (KerName.make mp2 lbl)
 
   let to_string kp = KerName.to_string (user kp)
   let print kp = str (to_string kp)
diff --git a/kernel/names.mli b/kernel/names.mli
index 2ea8108734..2145a51c4e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -274,9 +274,11 @@ sig
   type t
 
   (** Constructor and destructor *)
-  val make : ModPath.t -> DirPath.t -> Label.t -> t
+  val make : ModPath.t -> Label.t -> t
+  val repr : t -> ModPath.t * Label.t
+
   val make2 : ModPath.t -> Label.t -> t
-  val repr : t -> ModPath.t * DirPath.t * Label.t
+  [@@ocaml.deprecated "Please use [KerName.make]"]
 
   (** Projections *)
   val modpath : t -> ModPath.t
@@ -317,15 +319,12 @@ sig
   val make2 : ModPath.t -> Label.t -> t
   (** Shortcut for [(make1 (KerName.make2 ...))] *)
 
-  val make3 : ModPath.t -> DirPath.t -> Label.t -> t
-  (** Shortcut for [(make1 (KerName.make ...))] *)
-
   (** Projections *)
 
   val user : t -> KerName.t
   val canonical : t -> KerName.t
 
-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t
   (** Shortcut for [KerName.repr (user ...)] *)
 
   val modpath : t -> ModPath.t
@@ -403,15 +402,12 @@ sig
   val make2 : ModPath.t -> Label.t -> t
   (** Shortcut for [(make1 (KerName.make2 ...))] *)
 
-  val make3 : ModPath.t -> DirPath.t -> Label.t -> t
-  (** Shortcut for [(make1 (KerName.make ...))] *)
-
   (** Projections *)
 
   val user : t -> KerName.t
   val canonical : t -> KerName.t
 
-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t
   (** Shortcut for [KerName.repr (user ...)] *)
 
   val modpath : t -> ModPath.t
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 74b075f4a5..482a2f3a3c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function
 let list_of_mp mp = list_of_mp [] mp
 
 let string_of_kn kn =
-  let (mp,_dp,l) = KerName.repr kn in
+  let (mp,l) = KerName.repr kn in
   let mp = list_of_mp mp in
   String.concat "_" mp ^ "_" ^ string_of_label l
 
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 8ac3538fc5..5d1b882361 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -27,7 +27,7 @@ let rec translate_mod prefix mp env mod_expr acc =
 and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
-     let con = Constant.make3 mp DirPath.empty l in
+     let con = Constant.make2 mp l in
      (if !Flags.debug then
         let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
 	Feedback.msg_debug (Pp.str msg));
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b036aa6a67..b03342da39 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -479,10 +479,10 @@ type global_declaration =
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
 
-let add_constant_aux no_section senv (kn, cb) =
-  let l = pi3 (Constant.repr3 kn) in
+let add_constant_aux ~in_section senv (kn, cb) =
+  let l = Constant.label kn in
   let cb, otab = match cb.const_body with
-    | OpaqueDef lc when no_section ->
+    | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
       let od, otab =
@@ -505,13 +505,11 @@ let export_private_constants ~in_section ce senv =
   let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
   let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
-  let no_section = not in_section in
-  let senv = List.fold_left (add_constant_aux no_section) senv bodies in
+  let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_constant dir l decl senv =
-  let kn = Constant.make3 senv.modpath dir l in
-  let no_section = DirPath.is_empty dir in
+let add_constant ~in_section l decl senv =
+  let kn = Constant.make2 senv.modpath l in
   let senv =
     let cb = 
       match decl with
@@ -520,9 +518,9 @@ let add_constant dir l decl senv =
       | ConstantEntry (PureEntry, ce) ->
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
       | GlobalRecipe r ->
-        let cb = Term_typing.translate_recipe senv.env kn r in
-        if no_section then Declareops.hcons_const_body cb else cb in
-    add_constant_aux no_section senv (kn, cb) in
+        let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+        if in_section then cb else Declareops.hcons_const_body cb in
+    add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
 (** Insertion of inductive types *)
@@ -535,9 +533,9 @@ let check_mind mie lab =
     (* The label and the first inductive type name should match *)
     assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
 
-let add_mind dir l mie senv =
+let add_mind l mie senv =
   let () = check_mind mie l in
-  let kn = MutInd.make3 senv.modpath dir l in
+  let kn = MutInd.make2 senv.modpath l in
   let mib = Term_typing.translate_mind senv.env kn mie in
   let mib =
     match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
@@ -770,9 +768,9 @@ let add_include me is_module inl senv =
   let add senv ((l,elem) as field) =
     let new_name = match elem with
       | SFBconst _ ->
-        C (Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp_sup l))
+        C (Mod_subst.constant_of_delta_kn resolver (KerName.make mp_sup l))
       | SFBmind _ ->
-	I (Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp_sup l))
+        I (Mod_subst.mind_of_delta_kn resolver (KerName.make mp_sup l))
       | SFBmodule _ -> M
       | SFBmodtype _ -> MT
     in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6e0febaa3f..efb4957006 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -105,13 +105,13 @@ val export_private_constants : in_section:bool ->
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
 val add_constant :
-  DirPath.t -> Label.t -> global_declaration ->
+  in_section:bool -> Label.t -> global_declaration ->
     Constant.t safe_transformer
 
 (** Adding an inductive type *)
 
 val add_mind :
-  DirPath.t -> Label.t -> Entries.mutual_inductive_entry ->
+  Label.t -> Entries.mutual_inductive_entry ->
     MutInd.t safe_transformer
 
 (** Adding a module or a module type *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bfe68671a2..d64342dbb0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -103,8 +103,8 @@ let check_polymorphic_instance error env auctx1 auctx2 =
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
-  let kn1 = KerName.make2 mp1 l in
-  let kn2 = KerName.make2 mp2 l in
+  let kn1 = KerName.make mp1 l in
+  let kn2 = KerName.make mp2 l in
   let error why = error_signature_mismatch l spec2 why in
   let check_conv why cst poly f = check_conv_error error why cst poly f in
   let mib1 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 47247ff25e..5ccc23eefc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -531,11 +531,7 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     t
 
-let translate_recipe env kn r =
-  (** We only hashcons the term when outside of a section, otherwise this would
-      be useless. It is detected by the dirpath of the constant being empty. *)
-  let (_, dir, _) = Constant.repr3 kn in
-  let hcons = DirPath.is_empty dir in
+let translate_recipe ~hcons env kn r =
   build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
 
 let translate_local_def env _id centry =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b05e05e4dc..ab25090b00 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -64,7 +64,7 @@ val export_side_effects :
 val translate_mind :
   env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
-val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)