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

11 files changed, 31 insertions, 131 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 026b7aa316..e71de4d77e 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -119,29 +119,26 @@ let prelude_module_name = init_dir@["Prelude"]
 let prelude_module = make_dir prelude_module_name
 
 let logic_module_name = init_dir@["Logic"]
-let logic_module = make_dir logic_module_name
+let logic_module = MPfile (make_dir logic_module_name)
 
 let logic_type_module_name = init_dir@["Logic_Type"]
 let logic_type_module = make_dir logic_type_module_name
 
 let datatypes_module_name = init_dir@["Datatypes"]
-let datatypes_module = make_dir datatypes_module_name
+let datatypes_module = MPfile (make_dir datatypes_module_name)
 
 let jmeq_module_name = [coq;"Logic";"JMeq"]
-let jmeq_module = make_dir jmeq_module_name
-
-(* TODO: temporary hack. Works only if the module isn't an alias *)
-let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
-let make_con dir id = Globnames.encode_con dir (Id.of_string id)
+let jmeq_library_path = make_dir jmeq_module_name
+let jmeq_module = MPfile jmeq_library_path
 
 (** Identity *)
 
-let id = make_con datatypes_module "idProp"
-let type_of_id = make_con datatypes_module "IDProp"
+let id = Constant.make2 datatypes_module @@ Label.make "idProp"
+let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp"
 
 (** Natural numbers *)
-let nat_kn = make_ind datatypes_module "nat"
-let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
+let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat"
+let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat")
 
 let glob_nat = IndRef (nat_kn,0)
 
@@ -151,7 +148,7 @@ let glob_O = ConstructRef path_of_O
 let glob_S = ConstructRef path_of_S
 
 (** Booleans *)
-let bool_kn = make_ind datatypes_module "bool"
+let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool"
 
 let glob_bool = IndRef (bool_kn,0)
 
@@ -161,13 +158,13 @@ let glob_true  = ConstructRef path_of_true
 let glob_false  = ConstructRef path_of_false
 
 (** Equality *)
-let eq_kn = make_ind logic_module "eq"
+let eq_kn = MutInd.make2 logic_module @@ Label.make "eq"
 let glob_eq = IndRef (eq_kn,0)
 
-let identity_kn = make_ind datatypes_module "identity"
+let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity"
 let glob_identity = IndRef (identity_kn,0)
 
-let jmeq_kn = make_ind jmeq_module "JMeq"
+let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq"
 let glob_jmeq = IndRef (jmeq_kn,0)
 
 type coq_sigma_data = {
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 8844684957..6a3d0953cd 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -61,12 +61,13 @@ val init_modules : string list list
 (** Modules *)
 val prelude_module : DirPath.t
 
-val logic_module : DirPath.t
+val logic_module : ModPath.t
 val logic_module_name : string list
 
 val logic_type_module : DirPath.t
 
-val jmeq_module : DirPath.t
+val jmeq_module : ModPath.t
+val jmeq_library_path : DirPath.t
 val jmeq_module_name : string list
 
 val datatypes_module_name : string list
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0b3b461e6c..e01a99f731 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -164,8 +164,7 @@ module ModObjs :
 *)
 
 let mp_of_kn kn =
-  let mp,sec,l = KerName.repr kn in
-  assert (DirPath.is_empty sec);
+  let mp,l = KerName.repr kn in
   MPdot (mp,l)
 
 let dir_of_sp sp =
diff --git a/library/global.ml b/library/global.ml
index e872d081d6..0e236e6d34 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -91,8 +91,8 @@ let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
-let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
+let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
+let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
diff --git a/library/global.mli b/library/global.mli
index 5205968c7b..fd6c9a60d4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -42,9 +42,9 @@ val export_private_constants : in_section:bool ->
   unit Entries.definition_entry * Safe_typing.exported_private_constant list
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t
+  in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t
 val add_mind :
-  DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t
+  Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
 (** Extra universe constraints *)
 val add_constraints : Univ.Constraint.t -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index 6bbdd36489..9aca7788d2 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -8,11 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Names
 open Constr
 open Mod_subst
-open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
 type global_reference = GlobRef.t =
@@ -137,53 +135,5 @@ type global_reference_or_constr =
   | IsGlobal of global_reference
   | IsConstr of constr
 
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-let encode_mind dir id = MutInd.make2 (MPfile dir) (Label.of_id id)
-
-let encode_con dir id = Constant.make2 (MPfile dir) (Label.of_id id)
-
-let check_empty_section dp =
-  if not (DirPath.is_empty dp) then
-    anomaly (Pp.str "Section part should be empty!")
-
-let decode_mind kn =
-  let rec dir_of_mp = function
-    | MPfile dir -> DirPath.repr dir
-    | MPbound mbid ->
-	let _,_,dp = MBId.repr mbid in
-	let id = MBId.to_id mbid in
-	  id::(DirPath.repr dp)
-    | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
-  in
-  let mp,sec_dir,l = MutInd.repr3 kn in
-  check_empty_section sec_dir;
-  (DirPath.make (dir_of_mp mp)),Label.to_id l
-
-let decode_con kn =
-  let mp,sec_dir,l = Constant.repr3 kn in
-  check_empty_section sec_dir;
-  match mp with
-    | MPfile dir -> (dir,Label.to_id l)
-    | _ -> anomaly (Pp.str "MPfile expected!")
-
-(** Popping one level of section in global names.
-    These functions are meant to be used during discharge:
-    user and canonical kernel names must be equal. *)
-
-let pop_con con =
-  let (mp,dir,l) = Constant.repr3 con in
-  Constant.make3 mp (pop_dirpath dir) l
-
-let pop_kn kn =
-  let (mp,dir,l) = MutInd.repr3 kn in
-  MutInd.make3 mp (pop_dirpath dir) l
-
-let pop_global_reference = function
-  | ConstRef con -> ConstRef (pop_con con)
-  | IndRef (kn,i) -> IndRef (pop_kn kn,i)
-  | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
-  | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
-
 (* Deprecated *)
 let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index 45ee069b06..a96a42ced2 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -82,15 +82,3 @@ end
 type global_reference_or_constr = 
   | IsGlobal of GlobRef.t
   | IsConstr of constr
-
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-val encode_mind : DirPath.t -> Id.t -> MutInd.t
-val decode_mind : MutInd.t -> DirPath.t * Id.t
-val encode_con : DirPath.t -> Id.t -> Constant.t
-val decode_con : Constant.t -> DirPath.t * Id.t
-
-(** {6 Popping one level of section in global names } *)
-val pop_con : Constant.t -> Constant.t
-val pop_kn : MutInd.t-> MutInd.t
-val pop_global_reference : GlobRef.t -> GlobRef.t
diff --git a/library/keys.ml b/library/keys.ml
index a74d13c600..53447a679a 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -92,8 +92,7 @@ let subst_keys (subst,(k,k')) =
   (subst_key subst k, subst_key subst k')
 
 let discharge_key = function
-  | KGlob g when Lib.is_in_section g ->
-    if isVarRef g then None else Some (KGlob (pop_global_reference g))
+  | KGlob (VarRef _ as g) when Lib.is_in_section g -> None
   | x -> Some x
 
 let discharge_keys (_,(k,k')) =
diff --git a/library/lib.ml b/library/lib.ml
index 07026a9c2a..27c5056a7f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -135,8 +135,8 @@ let make_path_except_section id =
   Libnames.make_path (cwd_except_section ()) id
 
 let make_kn id =
-  let mp, dir = current_mp (), current_sections () in
-  Names.KerName.make mp dir (Names.Label.of_id id)
+  let mp = current_mp () in
+  Names.KerName.make mp (Names.Label.of_id id)
 
 let make_oname id = Libnames.make_oname !lib_state.path_prefix id
 
@@ -632,44 +632,12 @@ let library_part = function
   |VarRef id -> library_dp ()
   |ref -> dp_of_mp (mp_of_global ref)
 
-(************************)
-(* Discharging names *)
-
-let con_defined_in_sec kn =
-  let _,dir,_ = Names.Constant.repr3 kn in
-  not (Names.DirPath.is_empty dir) &&
-  Names.DirPath.equal (pop_dirpath dir) (current_sections ())
-
-let defined_in_sec kn =
-  let _,dir,_ = Names.MutInd.repr3 kn in
-  not (Names.DirPath.is_empty dir) &&
-  Names.DirPath.equal (pop_dirpath dir) (current_sections ())
-
-let discharge_global = function
-  | ConstRef kn when con_defined_in_sec kn ->
-      ConstRef (Globnames.pop_con kn)
-  | IndRef (kn,i) when defined_in_sec kn ->
-      IndRef (Globnames.pop_kn kn,i)
-  | ConstructRef ((kn,i),j) when defined_in_sec kn ->
-      ConstructRef ((Globnames.pop_kn kn,i),j)
-  | r -> r
-
-let discharge_kn kn =
-  if defined_in_sec kn then Globnames.pop_kn kn else kn
-
-let discharge_con cst =
-  if con_defined_in_sec cst then Globnames.pop_con cst else cst
-
 let discharge_proj_repr =
   Projection.Repr.map_npars (fun mind npars ->
-      if not (defined_in_sec mind) then mind, npars
-      else
-        let modlist = replacement_context () in
-        let _, newpars = Mindmap.find mind (snd modlist) in
-        Globnames.pop_kn mind, npars + Array.length newpars)
-
-let discharge_inductive (kn,i) =
-  (discharge_kn kn,i)
+      if not (is_in_section (IndRef (mind,0))) then mind, npars
+      else let modlist = replacement_context () in
+      let _, newpars = Mindmap.find mind (snd modlist) in
+      mind, npars + Array.length newpars)
 
 let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
   let open Univ in
diff --git a/library/lib.mli b/library/lib.mli
index a7d21060e9..686e6a0e2d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -187,10 +187,8 @@ val is_polymorphic_univ : Univ.Level.t -> bool
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
-val discharge_kn :  MutInd.t -> MutInd.t
-val discharge_con : Constant.t -> Constant.t
+(* XXX Why can't we use the kernel functions ? *)
+
 val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
-val discharge_global : GlobRef.t -> GlobRef.t
-val discharge_inductive : inductive -> inductive
 val discharge_abstract_universe_context :
   abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/library/libnames.ml b/library/libnames.ml
index 23085048a1..bd2ca550b9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -171,8 +171,8 @@ type object_prefix = {
 }
 
 (* let make_oname (dirpath,(mp,dir)) id = *)
-let make_oname { obj_dir; obj_mp; obj_sec } id =
-  make_path obj_dir id, KerName.make obj_mp obj_sec (Label.of_id id)
+let make_oname { obj_dir; obj_mp } id =
+  make_path obj_dir id, KerName.make obj_mp (Label.of_id id)
 
 (* to this type are mapped DirPath.t's in the nametab *)
 type global_dir_reference =