Merge PR #6065: [api] Deprecate all legacy uses of Names in core.

13 files changed, 107 insertions, 107 deletions

diff --git a/library/coqlib.mli b/library/coqlib.mli
index b560cabb6..cc22f1635 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -71,8 +71,8 @@ val jmeq_module_name : string list
 val datatypes_module_name : string list
 
 (** Identity  *)
-val id : constant
-val type_of_id : constant
+val id : Constant.t
+val type_of_id : Constant.t
 
 (** Natural numbers *)
 val nat_path : full_path
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 6d9295bde..cda40f49f 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -39,7 +39,7 @@ let inl2intopt = function
 
 type algebraic_objects =
   | Objs of Lib.lib_objects
-  | Ref of module_path * substitution
+  | Ref of ModPath.t * substitution
 
 type substitutive_objects = MBId.t list * algebraic_objects
 
@@ -62,9 +62,9 @@ type substitutive_objects = MBId.t list * algebraic_objects
 
 module ModSubstObjs :
  sig
-   val set : module_path -> substitutive_objects -> unit
-   val get : module_path -> substitutive_objects
-   val set_missing_handler : (module_path -> substitutive_objects) -> unit
+   val set : ModPath.t -> substitutive_objects -> unit
+   val get : ModPath.t -> substitutive_objects
+   val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit
  end =
  struct
    let table =
@@ -126,8 +126,8 @@ type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects
 
 module ModObjs :
  sig
-   val set : module_path -> module_objects -> unit
-   val get : module_path -> module_objects (* may raise Not_found *)
+   val set : ModPath.t -> module_objects -> unit
+   val get : ModPath.t -> module_objects (* may raise Not_found *)
    val all : unit -> module_objects MPmap.t
  end =
  struct
@@ -143,11 +143,11 @@ module ModObjs :
 (** {6 Name management}
 
     Auxiliary functions to transform full_path and kernel_name given
-    by Lib into module_path and DirPath.t needed for modules
+    by Lib into ModPath.t and DirPath.t needed for modules
 *)
 
 let mp_of_kn kn =
-  let mp,sec,l = repr_kn kn in
+  let mp,sec,l = KerName.repr kn in
   assert (DirPath.is_empty sec);
   MPdot (mp,l)
 
@@ -336,8 +336,8 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs
 
 (** {6 From module expression to substitutive objects} *)
 
-(** Turn a chain of [MSEapply] into the head module_path and the
-    list of module_path parameters (deepest param coming first).
+(** Turn a chain of [MSEapply] into the head ModPath.t and the
+    list of ModPath.t parameters (deepest param coming first).
     The left part of a [MSEapply] must be either [MSEident] or
     another [MSEapply]. *)
 
@@ -911,7 +911,7 @@ let subst_import (subst,(export,mp as obj)) =
   let mp' = subst_mp subst mp in
   if mp'==mp then obj else (export,mp')
 
-let in_import : bool * module_path -> obj =
+let in_import : bool * ModPath.t -> obj =
   declare_object {(default_object "IMPORT MODULE") with
     cache_function = cache_import;
     open_function = open_import;
@@ -961,7 +961,7 @@ let debug_print_modtab _ =
     | l -> str "[." ++ int (List.length l) ++ str ".]"
   in
   let pr_modinfo mp (prefix,substobjs,keepobjs) s =
-    s ++ str (string_of_mp mp) ++ (spc ())
+    s ++ str (ModPath.to_string mp) ++ (spc ())
     ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs)))
   in
   let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 9d750b616..90e86cd02 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -30,15 +30,15 @@ val declare_module :
   Id.t ->
   'modast module_params ->
   ('modast * inline) module_signature ->
-  ('modast * inline) list -> module_path
+  ('modast * inline) list -> ModPath.t
 
 val start_module :
   'modast module_interpretor ->
   bool option -> Id.t ->
   'modast module_params ->
-  ('modast * inline) module_signature -> module_path
+  ('modast * inline) module_signature -> ModPath.t
 
-val end_module : unit -> module_path
+val end_module : unit -> ModPath.t
 
 
 
@@ -53,15 +53,15 @@ val declare_modtype :
   'modast module_params ->
   ('modast * inline) list ->
   ('modast * inline) list ->
-  module_path
+  ModPath.t
 
 val start_modtype :
   'modast module_interpretor ->
   Id.t ->
   'modast module_params ->
-  ('modast * inline) list -> module_path
+  ('modast * inline) list -> ModPath.t
 
-val end_modtype : unit -> module_path
+val end_modtype : unit -> ModPath.t
 
 (** {6 Libraries i.e. modules on disk } *)
 
@@ -90,13 +90,13 @@ val append_end_library_hook : (unit -> unit) -> unit
    every object of the module. Raises [Not_found] when [mp] is unknown
    or when [mp] corresponds to a functor. *)
 
-val really_import_module : module_path -> unit
+val really_import_module : ModPath.t -> unit
 
 (** [import_module export mp] is a synchronous version of
    [really_import_module]. If [export] is [true], the module is also
    opened every time the module containing it is. *)
 
-val import_module : bool -> module_path -> unit
+val import_module : bool -> ModPath.t -> unit
 
 (** Include  *)
 
diff --git a/library/decls.mli b/library/decls.mli
index 478f0bca0..524377257 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -30,8 +30,8 @@ val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)
 
-val add_constant_kind : constant -> logical_kind -> unit
-val constant_kind : constant -> logical_kind
+val add_constant_kind : Constant.t -> logical_kind -> unit
+val constant_kind : Constant.t -> logical_kind
 
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
diff --git a/library/global.mli b/library/global.mli
index 15bf58f82..1aff0a376 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -39,9 +39,9 @@ val export_private_constants : in_section:bool ->
   unit Entries.constant_entry * Safe_typing.exported_private_constant list
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+  DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t
 val add_mind :
-  DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
+  DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
 (** Extra universe constraints *)
 val add_constraints : Univ.constraints -> unit
@@ -53,23 +53,23 @@ val push_context_set : bool -> Univ.universe_context_set -> unit
 
 val add_module :
   Id.t -> Entries.module_entry -> Declarations.inline ->
-    module_path * Mod_subst.delta_resolver
+    ModPath.t * Mod_subst.delta_resolver
 val add_modtype :
-  Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path
+  Id.t -> Entries.module_type_entry -> Declarations.inline -> ModPath.t
 val add_include :
   Entries.module_struct_entry -> bool -> Declarations.inline ->
     Mod_subst.delta_resolver
 
 (** Interactive modules and module types *)
 
-val start_module : Id.t -> module_path
-val start_modtype : Id.t -> module_path
+val start_module : Id.t -> ModPath.t
+val start_modtype : Id.t -> ModPath.t
 
 val end_module : Summary.frozen -> Id.t ->
   (Entries.module_struct_entry * Declarations.inline) option ->
-    module_path * MBId.t list * Mod_subst.delta_resolver
+    ModPath.t * MBId.t list * Mod_subst.delta_resolver
 
-val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list
+val end_modtype : Summary.frozen -> Id.t -> ModPath.t * MBId.t list
 
 val add_module_parameter :
   MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
@@ -78,22 +78,22 @@ val add_module_parameter :
 (** {6 Queries in the global environment } *)
 
 val lookup_named     : variable -> Context.Named.Declaration.t
-val lookup_constant  : constant -> Declarations.constant_body
+val lookup_constant  : Constant.t -> Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
 val lookup_pinductive : Constr.pinductive -> 
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
-val lookup_mind      : mutual_inductive -> Declarations.mutual_inductive_body
-val lookup_module    : module_path -> Declarations.module_body
-val lookup_modtype   : module_path -> Declarations.module_type_body
+val lookup_mind      : MutInd.t -> Declarations.mutual_inductive_body
+val lookup_module    : ModPath.t -> Declarations.module_body
+val lookup_modtype   : ModPath.t -> Declarations.module_type_body
 val exists_objlabel  : Label.t -> bool
 
-val constant_of_delta_kn : kernel_name -> constant
-val mind_of_delta_kn : kernel_name -> mutual_inductive
+val constant_of_delta_kn : KerName.t -> Constant.t
+val mind_of_delta_kn : KerName.t -> MutInd.t
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
 
-val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option
+val body_of_constant : Constant.t -> (Term.constr * Univ.AUContext.t) option
 (** Returns the body of the constant if it has any, and the polymorphic context
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
@@ -111,12 +111,12 @@ val set_global_universe_names : universe_names -> unit
 
 (** {6 Compiled libraries } *)
 
-val start_library : DirPath.t -> module_path
+val start_library : DirPath.t -> ModPath.t
 val export : ?except:Future.UUIDSet.t -> DirPath.t ->
-  module_path * Safe_typing.compiled_library * Safe_typing.native_library
+  ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
-  module_path
+  ModPath.t
 
 (** {6 Misc } *)
 
@@ -154,16 +154,16 @@ val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_c
 val register :
   Retroknowledge.field -> Term.constr -> Term.constr -> unit
 
-val register_inline : constant -> unit
+val register_inline : Constant.t -> unit
 
 (** {6 Oracle } *)
 
-val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit
+val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
 (* Modifies the global state, registering new universes *)
 
-val current_dirpath : unit -> Names.dir_path
+val current_dirpath : unit -> DirPath.t
 
-val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a
+val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
 
 val global_env_summary_name : string
diff --git a/library/globnames.ml b/library/globnames.ml
index 5c75994dd..9f652896c 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -15,7 +15,7 @@ open Libnames
 (*s Global reference is a kernel side type for all references together *)
 type global_reference =
   | VarRef of variable           (** A reference to the section-context. *)
-  | ConstRef of constant         (** A reference to the environment. *)
+  | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
   | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
 
@@ -26,7 +26,7 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false
 
 let eq_gr gr1 gr2 =
   gr1 == gr2 || match gr1,gr2 with
-    | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
+    | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2
     | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
     | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
     | VarRef v1, VarRef v2 -> Id.equal v1 v2
@@ -67,9 +67,9 @@ let subst_global subst ref = match ref with
 	if c'==c then ref,t else ConstructRef c', t
 
 let canonical_gr = function
-  | ConstRef con -> ConstRef(constant_of_kn(canonical_con con))
-  | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i)
-  | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+  | ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con))
+  | IndRef (kn,i) -> IndRef(MutInd.make1(MutInd.canonical kn),i)
+  | ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j)
   | VarRef id -> VarRef id
 
 let global_of_constr c = match kind_of_term c with
@@ -81,7 +81,7 @@ let global_of_constr c = match kind_of_term c with
 
 let is_global c t =
   match c, kind_of_term t with
-  | ConstRef c, Const (c', _) -> eq_constant c c'
+  | ConstRef c, Const (c', _) -> Constant.equal c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
   | VarRef id, Var id' -> Id.equal id id'
@@ -157,7 +157,7 @@ module Refset_env = Refmap_env.Set
 
 (* Extended global references *)
 
-type syndef_name = kernel_name
+type syndef_name = KerName.t
 
 type extended_global_reference =
   | TrueGlobal of global_reference
@@ -180,7 +180,7 @@ module ExtRefOrdered = struct
     if x == y then 0
     else match x, y with
       | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry
-      | SynDef knx, SynDef kny -> kn_ord knx kny
+      | SynDef knx, SynDef kny -> KerName.compare knx kny
       | TrueGlobal _, SynDef _ -> -1
       | SynDef _, TrueGlobal _ -> 1
 
@@ -215,12 +215,12 @@ let decode_mind kn =
 	  id::(DirPath.repr dp)
     | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
   in
-  let mp,sec_dir,l = repr_mind kn 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 = repr_con kn in
+  let mp,sec_dir,l = Constant.repr3 kn in
   check_empty_section sec_dir;
   match mp with
     | MPfile dir -> (dir,Label.to_id l)
@@ -231,12 +231,12 @@ let decode_con kn =
     user and canonical kernel names must be equal. *)
 
 let pop_con con =
-  let (mp,dir,l) = repr_con con in
-  Names.make_con mp (pop_dirpath dir) l
+  let (mp,dir,l) = Constant.repr3 con in
+  Constant.make3 mp (pop_dirpath dir) l
 
 let pop_kn kn =
-  let (mp,dir,l) = repr_mind kn in
-  Names.make_mind mp (pop_dirpath dir) l
+  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)
diff --git a/library/globnames.mli b/library/globnames.mli
index 0b5971b6e..361631bd3 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -14,7 +14,7 @@ open Mod_subst
 (** {6 Global reference is a kernel side type for all references together } *)
 type global_reference =
   | VarRef of variable           (** A reference to the section-context. *)
-  | ConstRef of constant         (** A reference to the environment. *)
+  | ConstRef of Constant.t       (** A reference to the environment. *)
   | IndRef of inductive          (** A reference to an inductive type. *)
   | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
 
@@ -27,7 +27,7 @@ val eq_gr : global_reference -> global_reference -> bool
 val canonical_gr : global_reference -> global_reference
 
 val destVarRef : global_reference -> variable
-val destConstRef : global_reference -> constant
+val destConstRef : global_reference -> Constant.t
 val destIndRef : global_reference -> inductive
 val destConstructRef : global_reference -> constructor
 
@@ -72,7 +72,7 @@ module Refmap_env : Map.ExtS
 
 (** {6 Extended global references } *)
 
-type syndef_name = kernel_name
+type syndef_name = KerName.t
 
 type extended_global_reference =
   | TrueGlobal of global_reference
@@ -91,13 +91,13 @@ type global_reference_or_constr =
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
-val encode_mind : DirPath.t -> Id.t -> mutual_inductive
-val decode_mind : mutual_inductive -> DirPath.t * Id.t
-val encode_con : DirPath.t -> Id.t -> constant
-val decode_con : constant -> DirPath.t * Id.t
+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 -> constant
-val pop_kn : mutual_inductive-> mutual_inductive
+val pop_con : Constant.t -> Constant.t
+val pop_kn : MutInd.t-> MutInd.t
 val pop_global_reference : global_reference -> global_reference
diff --git a/library/heads.ml b/library/heads.ml
index c12fa9479..d2cfc0990 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -25,7 +25,7 @@ open Context.Named.Declaration
    the evaluation of [phi(0)] and the head of [h] is declared unknown). *)
 
 type rigid_head_kind =
-| RigidParameter of constant (* a Const without body *)
+| RigidParameter of Constant.t (* a Const without body *)
 | RigidVar of variable (* a Var without body *)
 | RigidType (* an inductive, a product or a sort *)
 
@@ -156,7 +156,7 @@ let cache_head o =
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
       let cst,c = subst_con_kn subst cst in
-      if isConst c && eq_constant (fst (destConst c)) cst then
+      if isConst c && Constant.equal (fst (destConst c)) cst then
         (* A change of the prefix of the constant *)
         k
       else
diff --git a/library/lib.ml b/library/lib.ml
index e95bb47f2..a6fa27be8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -62,7 +62,7 @@ let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn),Leaf o) :: stk ->
-	let id = Names.Label.to_id (Names.label kn) in
+	let id = Names.Label.to_id (Names.KerName.label kn) in
 	  (match classify_object o with
 	     | Dispose -> clean acc stk
 	     | Keep o' ->
@@ -93,12 +93,12 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *)
 
-let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
+let initial_prefix = default_library,(Names.ModPath.initial,Names.DirPath.empty)
 
 type lib_state = {
   comp_name   : Names.DirPath.t option;
   lib_stk     : library_segment;
-  path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t);
+  path_prefix : Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t);
 }
 
 let initial_lib_state = {
@@ -137,7 +137,7 @@ let make_path_except_section id =
 
 let make_kn id =
   let mp,dir = current_prefix () in
-  Names.make_kn mp dir (Names.Label.of_id id)
+  Names.KerName.make mp dir (Names.Label.of_id id)
 
 let make_oname id = Libnames.make_oname !lib_state.path_prefix id
 
@@ -226,7 +226,7 @@ let add_anonymous_entry node =
   add_entry (make_oname (anonymous_id ())) node
 
 let add_leaf id obj =
-  if Names.ModPath.equal (current_mp ()) Names.initial_path then
+  if Names.ModPath.equal (current_mp ()) Names.ModPath.initial then
     user_err Pp.(str "No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -597,7 +597,7 @@ let init () =
 
 let mp_of_global = function
   |VarRef id -> current_mp ()
-  |ConstRef cst -> Names.con_modpath cst
+  |ConstRef cst -> Names.Constant.modpath cst
   |IndRef ind -> Names.ind_modpath ind
   |ConstructRef constr -> Names.constr_modpath constr
 
@@ -621,12 +621,12 @@ let library_part = function
 (* Discharging names *)
 
 let con_defined_in_sec kn =
-  let _,dir,_ = Names.repr_con kn in
+  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.repr_mind kn in
+  let _,dir,_ = Names.MutInd.repr3 kn in
   not (Names.DirPath.is_empty dir) &&
   Names.DirPath.equal (pop_dirpath dir) (current_sections ())
 
diff --git a/library/lib.mli b/library/lib.mli
index 3dcec1d53..f941fd6d4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -81,8 +81,8 @@ val make_path : Names.Id.t -> Libnames.full_path
 val make_path_except_section : Names.Id.t -> Libnames.full_path
 
 (** Kernel-side names *)
-val current_mp : unit -> Names.module_path
-val make_kn : Names.Id.t -> Names.kernel_name
+val current_mp : unit -> Names.ModPath.t
+val make_kn : Names.Id.t -> Names.KerName.t
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -103,11 +103,11 @@ val find_opening_node : Names.Id.t -> node
 (** {6 Modules and module types } *)
 
 val start_module :
-  export -> Names.module_ident -> Names.module_path ->
+  export -> Names.module_ident -> Names.ModPath.t ->
   Summary.frozen -> Libnames.object_prefix
 
 val start_modtype :
-  Names.module_ident -> Names.module_path ->
+  Names.module_ident -> Names.ModPath.t ->
   Summary.frozen -> Libnames.object_prefix
 
 val end_module :
@@ -122,7 +122,7 @@ val end_modtype :
 
 (** {6 Compilation units } *)
 
-val start_compilation : Names.DirPath.t -> Names.module_path -> unit
+val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
 val end_compilation_checks : Names.DirPath.t -> Libnames.object_name
 val end_compilation :
   Libnames.object_name-> Libnames.object_prefix * library_segment
@@ -132,8 +132,8 @@ val end_compilation :
 val library_dp : unit -> Names.DirPath.t
 
 (** Extract the library part of a name even if in a section *)
-val dp_of_mp : Names.module_path -> Names.DirPath.t
-val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list
+val dp_of_mp : Names.ModPath.t -> Names.DirPath.t
+val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
 val library_part :  Globnames.global_reference -> Names.DirPath.t
 
 (** {6 Sections } *)
@@ -158,8 +158,8 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.
 val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Context.Named.t
 
-val section_segment_of_constant : Names.constant -> abstr_info
-val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
+val section_segment_of_constant : Names.Constant.t -> abstr_info
+val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info
 val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
 
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
@@ -168,15 +168,15 @@ val is_in_section : Globnames.global_reference -> bool
 val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
 val add_section_context : Univ.universe_context_set -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
-  Names.constant -> Context.Named.t -> unit
+  Names.Constant.t -> Context.Named.t -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  Names.mutual_inductive -> Context.Named.t -> unit
+  Names.MutInd.t -> Context.Named.t -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
-val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
-val discharge_con : Names.constant -> Names.constant
+val discharge_kn :  Names.MutInd.t -> Names.MutInd.t
+val discharge_con : Names.Constant.t -> Names.Constant.t
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
 val discharge_abstract_universe_context :
diff --git a/library/libnames.ml b/library/libnames.ml
index 0453f15e8..efb1348ab 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -154,12 +154,12 @@ let qualid_of_dirpath dir =
   let (l,a) = split_dirpath dir in
   make_qualid l a
 
-type object_name = full_path * kernel_name
+type object_name = full_path * KerName.t
 
-type object_prefix = DirPath.t * (module_path * DirPath.t)
+type object_prefix = DirPath.t * (ModPath.t * DirPath.t)
 
 let make_oname (dirpath,(mp,dir)) id =
-  make_path dirpath id, make_kn mp dir (Label.of_id id)
+  make_path dirpath id, KerName.make mp dir (Label.of_id id)
 
 (* to this type are mapped DirPath.t's in the nametab *)
 type global_dir_reference =
@@ -173,7 +173,7 @@ type global_dir_reference =
 let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
   DirPath.equal d1 d2 &&
   DirPath.equal p1 p2 &&
-  mp_eq mp1 mp2
+  ModPath.equal mp1 mp2
 
 let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
diff --git a/library/libnames.mli b/library/libnames.mli
index 1b351290a..ab2585334 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -91,9 +91,9 @@ val qualid_of_ident : Id.t -> qualid
    can be substituted and a "syntactic" [full_path] which can be printed
 *)
 
-type object_name = full_path * kernel_name
+type object_name = full_path * KerName.t
 
-type object_prefix = DirPath.t * (module_path * DirPath.t)
+type object_prefix = DirPath.t * (ModPath.t * DirPath.t)
 
 val eq_op : object_prefix -> object_prefix -> bool
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 3a380637c..c02447a7c 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -74,7 +74,7 @@ val error_global_not_found : ?loc:Loc.t -> qualid -> 'a
 type visibility = Until of int | Exactly of int
 
 val push : visibility -> full_path -> global_reference -> unit
-val push_modtype : visibility -> full_path -> module_path -> unit
+val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
@@ -85,11 +85,11 @@ val push_syndef : visibility -> full_path -> syndef_name -> unit
 
 val locate : qualid -> global_reference
 val locate_extended : qualid -> extended_global_reference
-val locate_constant : qualid -> constant
+val locate_constant : qualid -> Constant.t
 val locate_syndef : qualid -> syndef_name
-val locate_modtype : qualid -> module_path
+val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> global_dir_reference
-val locate_module : qualid -> module_path
+val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
 
 (** These functions globalize user-level references into global
@@ -105,7 +105,7 @@ val global_inductive : reference -> inductive
 val locate_all : qualid -> global_reference list
 val locate_extended_all : qualid -> extended_global_reference list
 val locate_extended_all_dir : qualid -> global_dir_reference list
-val locate_extended_all_modtype : qualid -> module_path list
+val locate_extended_all_modtype : qualid -> ModPath.t list
 
 (** Mapping a full path to a global reference *)
 
@@ -135,8 +135,8 @@ val full_name_module : qualid -> DirPath.t
 
 val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
-val dirpath_of_module : module_path -> DirPath.t
-val path_of_modtype : module_path -> full_path
+val dirpath_of_module : ModPath.t -> DirPath.t
+val path_of_modtype : ModPath.t -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -156,8 +156,8 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t
 
 val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
 val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
-val shortest_qualid_of_modtype : module_path -> qualid
-val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_modtype : ModPath.t -> qualid
+val shortest_qualid_of_module : ModPath.t -> qualid
 
 (** Deprecated synonyms *)