[api] Deprecate all legacy uses of Names in core.

This will allow to merge back `Names` with `API.Names`

134 files changed, 753 insertions, 750 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 753fd0fc0..354650964 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -81,7 +81,7 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 type 'a puniverses = 'a Univ.puniverses
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -127,12 +127,12 @@ type section_context = unit
 
 type delta_hint =
   | Inline of int * constr option
-  | Equiv of kernel_name
+  | Equiv of KerName.t
 
-type delta_resolver = module_path MPmap.t * delta_hint KNmap.t
+type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
 
 type 'a umap_t = 'a MPmap.t * 'a MBImap.t
-type substitution = (module_path * delta_resolver) umap_t
+type substitution = (ModPath.t * delta_resolver) umap_t
 
 (** {6 Delayed constr} *)
 
@@ -194,7 +194,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : mutual_inductive;
+  proj_ind : MutInd.t;
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
@@ -241,7 +241,7 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * constant array * projection_body array) option
+type record_body = (Id.t * Constant.t array * projection_body array) option
     (* The body is empty for non-primitive records, otherwise we get its
        binder name in projections and list of projections if it is primitive. *)
 
@@ -347,12 +347,12 @@ type ('ty,'a) functorize =
     only for short module printing and for extraction. *)
 
 type with_declaration =
-  | WithMod of Id.t list * module_path
+  | WithMod of Id.t list * ModPath.t
   | WithDef of Id.t list * (constr * Univ.universe_context)
 
 type module_alg_expr =
-  | MEident of module_path
-  | MEapply of module_alg_expr * module_path
+  | MEident of ModPath.t
+  | MEapply of module_alg_expr * ModPath.t
   | MEwith of module_alg_expr * with_declaration
 
 (** A component of a module structure *)
@@ -386,7 +386,7 @@ and module_implementation =
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 and 'a generic_module_body =
-  { mod_mp : module_path; (** absolute path of the module *)
+  { mod_mp : ModPath.t; (** absolute path of the module *)
     mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
diff --git a/checker/closure.ml b/checker/closure.ml
index 70718bfdc..7982ffa7a 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -63,7 +63,7 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
+  val fCONST : Constant.t -> red_kind
   val fVAR : Id.t -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
@@ -86,7 +86,7 @@ module RedFlags = (struct
     r_iota : bool }
 
   type red_kind = BETA | DELTA | IOTA | ZETA
-	      | CONST of constant | VAR of Id.t
+	      | CONST of Constant.t | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fIOTA = IOTA
@@ -165,7 +165,7 @@ type 'a tableKey =
   | VarKey of Id.t
   | RelKey of int
 
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 module KeyHash =
 struct
@@ -281,9 +281,9 @@ and fterm =
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (name * constr) list * constr * fconstr subs
-  | FProd of name * fconstr * fconstr
-  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+  | FProd of Name.t * fconstr * fconstr
+  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *)
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
diff --git a/checker/closure.mli b/checker/closure.mli
index ed5bb3d09..957cc4adb 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -30,7 +30,7 @@ val all_opaque      : transparent_state
 val all_transparent : transparent_state
 
 val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> constant -> bool
+val is_transparent_constant : transparent_state -> Constant.t -> bool
 
 (* Sets of reduction kinds. *)
 module type RedFlagsSig = sig
@@ -42,7 +42,7 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
+  val fCONST : Constant.t -> red_kind
   val fVAR : Id.t -> red_kind
 
   (* No reduction at all *)
@@ -71,7 +71,7 @@ type 'a tableKey =
   | VarKey of Id.t
   | RelKey of int
 
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
@@ -100,9 +100,9 @@ type fterm =
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (name * constr) list * constr * fconstr subs
-  | FProd of name * fconstr * fconstr
-  | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
+  | FProd of Name.t * fconstr * fconstr
+  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential_key * fconstr array
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
@@ -142,7 +142,7 @@ val inject : constr -> fconstr
 val fterm_of : fconstr -> fterm
 val term_of_fconstr : fconstr -> constr
 val destFLambda :
-  (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
+  (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
 
 (* Global and local constant cache *)
 type clos_infos
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 6fc71bb94..7458b3e0b 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -34,12 +34,12 @@ val empty_delta_resolver : delta_resolver
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
-val add_mbid : MBId.t -> module_path -> substitution -> substitution
-val add_mp   : module_path -> module_path -> substitution -> substitution
-val map_mbid : MBId.t -> module_path -> substitution
-val map_mp   : module_path -> module_path -> substitution
-val mp_in_delta : module_path -> delta_resolver -> bool
-val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
+val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution
+val add_mp   : ModPath.t -> ModPath.t -> substitution -> substitution
+val map_mbid : MBId.t -> ModPath.t -> substitution
+val map_mp   : ModPath.t -> ModPath.t -> substitution
+val mp_in_delta : ModPath.t -> delta_resolver -> bool
+val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t
 
 val subst_const_body : constant_body subst_fun
 val subst_mind : mutual_inductive_body subst_fun
diff --git a/checker/environ.ml b/checker/environ.ml
index a0818012c..9db0d60e8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -8,7 +8,7 @@ open Declarations
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
-  env_inductives_eq : kernel_name  KNmap.t;
+  env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 8e8d0fd49..6bda838f8 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -6,7 +6,7 @@ open Cic
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
-  env_inductives_eq : kernel_name KNmap.t;
+  env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
@@ -34,7 +34,7 @@ val rel_context : env -> rel_context
 val lookup_rel : int -> env -> rel_declaration
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
-val push_rec_types : name array * constr array * 'a -> env -> env
+val push_rec_types : Name.t array * constr array * 'a -> env -> env
 
 (* Universes *)
 val universes : env -> Univ.universes
@@ -44,31 +44,31 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val check_constraints : Univ.constraints -> env -> bool
 
 (* Constants *)
-val lookup_constant : constant -> env -> Cic.constant_body
-val add_constant : constant -> Cic.constant_body -> env -> env
-val constant_type : env -> constant puniverses -> constr Univ.constrained
+val lookup_constant : Constant.t -> env -> Cic.constant_body
+val add_constant : Constant.t -> Cic.constant_body -> env -> env
+val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
 type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> constant puniverses -> constr
-val evaluable_constant : constant -> env -> bool
+val constant_value : env -> Constant.t puniverses -> constr
+val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : constant -> env -> bool
+val is_projection : Constant.t -> env -> bool
 val lookup_projection : projection -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
 
 val lookup_mind :
-  mutual_inductive -> env -> Cic.mutual_inductive_body
+  MutInd.t -> env -> Cic.mutual_inductive_body
 
 val add_mind :
-  mutual_inductive -> Cic.mutual_inductive_body -> env -> env
+  MutInd.t -> Cic.mutual_inductive_body -> env -> env
 
 (* Modules *)
 val add_modtype :
-  module_path -> Cic.module_type_body -> env -> env
+  ModPath.t -> Cic.module_type_body -> env -> env
 val shallow_add_module :
-  module_path -> Cic.module_body -> env -> env
-val shallow_remove_module : module_path -> env -> env
-val lookup_module : module_path -> env -> Cic.module_body
-val lookup_modtype : module_path -> env -> Cic.module_type_body
+  ModPath.t -> Cic.module_body -> env -> env
+val shallow_remove_module : ModPath.t -> env -> env
+val lookup_module : ModPath.t -> env -> Cic.module_body
+val lookup_modtype : ModPath.t -> env -> Cic.module_type_body
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index b0554989e..5d4c3ee99 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -12,8 +12,8 @@ open Cic
 open Environ
 (*i*)
 
-val prkn : kernel_name -> Pp.t
-val prcon : constant -> Pp.t
+val prkn : KerName.t -> Pp.t
+val prcon : Constant.t -> Pp.t
 
 (*s The different kinds of errors that may result of a malformed inductive
   definition. *)
@@ -34,4 +34,4 @@ exception InductiveError of inductive_error
 
 (*s The following function does checks on inductive declarations. *)
 
-val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env
+val check_inductive : env -> MutInd.t -> mutual_inductive_body -> env
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 8f605935d..0170bbc94 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -31,7 +31,7 @@ val type_of_inductive : env -> mind_specif puniverses -> constr
 (* Return type as quoted by the user *)
 val type_of_constructor : pconstructor -> mind_specif -> constr
 
-val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array
+val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 16a3792aa..c7af8b286 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit
+val check_module : Environ.env -> Names.ModPath.t -> Cic.module_body -> unit
diff --git a/checker/modops.mli b/checker/modops.mli
index 0efff63c8..b73557d92 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -15,7 +15,7 @@ open Environ
 (* Various operations on modules and module types *)
 
 val module_type_of_module :
-  module_path option -> module_body -> module_type_body
+  ModPath.t option -> module_body -> module_type_body
 
 val is_functor : ('ty,'a) functorize -> bool
 
@@ -24,24 +24,24 @@ val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
-val add_module_type : module_path -> module_type_body -> env -> env
+val add_module_type : ModPath.t -> module_type_body -> env -> env
 
-val strengthen : module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> ModPath.t -> module_type_body
 
-val subst_and_strengthen : module_body -> module_path -> module_body
+val subst_and_strengthen : module_body -> ModPath.t -> module_body
 
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
-val error_not_match : label -> structure_field_body -> 'a
+val error_not_match : Label.t -> structure_field_body -> 'a
 
 val error_with_module : unit -> 'a
 
-val error_no_such_label : label -> 'a
+val error_no_such_label : Label.t -> 'a
 
 val error_no_such_label_sub :
-  label -> module_path -> 'a
+  Label.t -> ModPath.t -> 'a
 
-val error_not_a_constant : label -> 'a
+val error_not_a_constant : Label.t -> 'a
 
-val error_not_a_module : label -> 'a
+val error_not_a_module : Label.t -> 'a
diff --git a/checker/term.mli b/checker/term.mli
index 679a56ee4..2524dff18 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -38,8 +38,8 @@ val fold_rel_context_outside :
 val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
-val compose_lam : (name * constr) list -> constr -> constr
-val decompose_lam : constr -> (name * constr) list * constr
+val compose_lam : (Name.t * constr) list -> constr -> constr
+val decompose_lam : constr -> (Name.t * constr) list * constr
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
 val mkProd_or_LetIn : rel_declaration -> constr -> constr
 val it_mkProd_or_LetIn : constr -> rel_context -> constr
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index c5a69efdc..5794d8713 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -52,14 +52,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * constr) * unsafe_judgment
+  | Generalization of (Name.t * constr) * unsafe_judgment
   | ActualType of unsafe_judgment * constr
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int
+  | IllFormedRecBody of guard_error * Name.t array * int
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * constr array
+      int * Name.t array * unsafe_judgment array * constr array
   | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index b5f14c718..f45144c23 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -54,14 +54,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * constr) * unsafe_judgment
+  | Generalization of (Name.t * constr) * unsafe_judgment
   | ActualType of unsafe_judgment * constr
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int
+  | IllFormedRecBody of guard_error * Name.t array * int
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * constr array
+      int * Name.t array * unsafe_judgment array * constr array
   | UnsatisfiedConstraints of Univ.constraints
 
 exception TypeError of env * type_error
@@ -96,9 +96,9 @@ val error_cant_apply_bad_type :
       unsafe_judgment -> unsafe_judgment array -> 'a
 
 val error_ill_formed_rec_body :
-  env -> guard_error -> name array -> int -> 'a
+  env -> guard_error -> Name.t array -> int -> 'a
 
 val error_ill_typed_rec_body  :
-  env -> int -> name array -> unsafe_judgment array -> constr array -> 'a
+  env -> int -> Name.t array -> unsafe_judgment array -> constr array -> 'a
 
 val error_unsatisfied_constraints : env -> Univ.constraints -> 'a
diff --git a/checker/values.ml b/checker/values.ml
index 86634fbd8..9e16c8435 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli
+MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli
 
 *)
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 35956477d..0d833d33b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -41,11 +41,11 @@ let pplab l = pp (pr_lab l)
 let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (ModPath.debug_to_string mp))
-let ppcon con = pp(debug_pr_con con)
-let ppproj con = pp(debug_pr_con (Projection.constant con))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
 let ppkn kn = pp(str (KerName.to_string kn))
-let ppmind kn = pp(debug_pr_mind kn)
-let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
 let ppsp sp = pp(pr_path sp)
 let ppqualid qid = pp(pr_qualid qid)
 let ppclindex cl = pp(Classops.pr_cl_index cl)
@@ -125,10 +125,10 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
 let pP s = pp (hov 0 s)
 
 let safe_pr_global = function
-  | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")")
-  | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
+  | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")")
+  | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
 			  int i ++ str ")")
-  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
+  | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
 				      int i ++ str "," ++ int j ++ str ")")
   | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")")
 
@@ -226,7 +226,7 @@ let ppenv e = pp
 let ppenvwithcst e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
-   str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x))
 
@@ -258,13 +258,13 @@ let constr_display csr =
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
   | Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
-  | Const (c,u) -> "Const("^(string_of_con c)^","^(universes_display u)^")"
+  | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
   | Ind ((sp,i),u) ->
-      "MutInd("^(string_of_mind sp)^","^(string_of_int i)^","^(universes_display u)^")"
+      "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"
   | Construct (((sp,i),j),u) ->
-      "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
+      "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
-  | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")"
+  | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
   | Case (ci,p,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display bl)^")"
@@ -432,7 +432,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_mind sp)
+      print_string (MutInd.debug_to_string sp)
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
@@ -441,7 +441,7 @@ let print_pure_constr csr =
 	| ("Coq"::_::l) -> l
 	| l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
-      print_string (debug_string_of_con sp)
+      print_string (Constant.debug_to_string sp)
 
   in
     try
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index afa94a63e..8e43bf6ed 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -10,11 +10,11 @@ let ppripos (ri,pos) =
   | Reloc_annot a ->
       let sp,i = a.ci.ci_ind in
       print_string
-	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
+	("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
-      print_string ("getglob "^(string_of_con kn)^"\n"));
+      print_string ("getglob "^(Constant.to_string kn)^"\n"));
    print_flush ()
 
 let print_vfix () = print_string "vfix"
@@ -32,7 +32,7 @@ let print_idkey idk =
   match idk with
   | ConstKey sp ->
       print_string "Cons(";
-      print_string (string_of_con sp);
+      print_string (Constant.to_string sp);
       print_string ")"
   | VarKey id -> print_string (Id.to_string id)
   | RelKey i -> print_string "~";print_int i
@@ -63,7 +63,7 @@ and ppatom a =
   | Aid idk -> print_idkey idk
   | Atype u -> print_string "Type(...)"
   | Aind(sp,i) ->  print_string "Ind(";
-      print_string (string_of_mind sp);
+      print_string (MutInd.to_string sp);
       print_string ","; print_int i;
       print_string ")"
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 4dbf6c18a..a4ad233b0 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -99,8 +99,8 @@ val mkProd : Name.t * t * t -> t
 val mkLambda : Name.t * t * t -> t
 val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
-val mkConst : constant -> t
-val mkConstU : constant * EInstance.t -> t
+val mkConst : Constant.t -> t
+val mkConstU : Constant.t * EInstance.t -> t
 val mkProj : (projection * t) -> t
 val mkInd : inductive -> t
 val mkIndU : inductive * EInstance.t -> t
@@ -157,7 +157,7 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types
 val destLambda : Evd.evar_map -> t -> Name.t * types * t
 val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
 val destApp : Evd.evar_map -> t -> t * t array
-val destConst : Evd.evar_map -> t -> constant * EInstance.t
+val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
diff --git a/engine/evd.mli b/engine/evd.mli
index 96e4b6acc..7576b3d5f 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -580,7 +580,7 @@ val update_sigma_env : evar_map -> env -> evar_map
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant
+val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
 val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index c548fc4ac..ff0b5a74e 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -61,9 +61,9 @@ let is_imported_ref = function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
-      let (mp,_,_) = repr_mind kn in is_imported_modpath mp
+      let (mp,_,_) = MutInd.repr3 kn in is_imported_modpath mp
   | ConstRef kn ->
-      let (mp,_,_) = repr_con kn in is_imported_modpath mp
+      let (mp,_,_) = Constant.repr3 kn in is_imported_modpath mp
 
 let is_global id =
   try
@@ -99,7 +99,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
     match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
     | Cast (c,_,_) | App (c,_) -> hdrec c
-    | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
+    | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
     | Const _ | Ind _ | Construct _ | Var _ as c ->
 	Some (basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
@@ -130,8 +130,8 @@ let hdchar env sigma c =
     match EConstr.kind sigma c with
     | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
     | Cast (c,_,_) | App (c,_) -> hdrec k c
-    | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
-    | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
+    | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
+    | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
     | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
diff --git a/engine/termops.ml b/engine/termops.ml
index 76f707f94..67533cce4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -31,7 +31,7 @@ let pr_sort_family = function
   | InProp -> (str "Prop")
   | InType -> (str "Type")
 
-let pr_con sp = str(string_of_con sp)
+let pr_con sp = str(Constant.to_string sp)
 
 let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
   let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
@@ -74,9 +74,9 @@ let rec pr_constr c = match kind_of_term c with
       (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
        prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
   | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
-  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
+  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
   | Construct (((sp,i),j),u) ->
-      str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+      str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
   | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
   | Case (ci,p,c,bl) -> v 0
       (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
diff --git a/engine/universes.ml b/engine/universes.ml
index 7f5bf24b7..0a2045a04 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -161,7 +161,7 @@ let compare_head_gen_proj env equ eqs eqc' m n =
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
       (match kind_of_term f with
-      | Const (p', u) when eq_constant (Projection.constant p) p' -> 
+      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
           let pb = Environ.lookup_projection p env in
           let npars = pb.Declarations.proj_npars in
 	  if Array.length args == npars + 1 then
diff --git a/engine/universes.mli b/engine/universes.mli
index 8b2217d44..3678ec94d 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -31,10 +31,10 @@ val set_remote_new_univ_level : universe_level RemoteCounter.installer
 
 (** Side-effecting functions creating new universe levels. *)
 
-val new_univ_level : Names.dir_path -> universe_level
-val new_univ : Names.dir_path -> universe
-val new_Type : Names.dir_path -> types
-val new_Type_sort : Names.dir_path -> sorts
+val new_univ_level : DirPath.t -> universe_level
+val new_univ : DirPath.t -> universe
+val new_Type : DirPath.t -> types
+val new_Type_sort : DirPath.t -> sorts
 
 val new_global_univ : unit -> universe in_universe_context_set
 val new_sort_in_family : sorts_family -> sorts
@@ -90,7 +90,7 @@ val fresh_instance_from : abstract_universe_context -> universe_instance option
 
 val fresh_sort_in_family : env -> sorts_family -> 
   sorts in_universe_context_set
-val fresh_constant_instance : env -> constant ->
+val fresh_constant_instance : env -> Constant.t ->
   pconstant in_universe_context_set
 val fresh_inductive_instance : env -> inductive ->
   pinductive in_universe_context_set
diff --git a/interp/declare.ml b/interp/declare.ml
index bd8f3db50..0ead94eff 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -136,31 +136,31 @@ let check_exists sp =
 
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
-  let _,dir,_ = repr_kn kn in
+  let _,dir,_ = KerName.repr kn in
   let kn' =
     match obj.cst_decl with
     | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
-      then constant_of_kn kn
+      then Constant.make1 kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     | Some decl ->
       let () = check_exists sp in
       Global.add_constant dir id decl
   in
-  assert (eq_constant kn' (constant_of_kn kn));
-  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+  assert (Constant.equal kn' (Constant.make1 kn));
+  Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
   add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
-  add_constant_kind (constant_of_kn kn) obj.cst_kind
+  add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharged_hyps kn sechyps =
-  let (_,dir,_) = repr_kn kn in
+  let (_,dir,_) = KerName.repr kn in
   let args = Array.to_list (instance_from_variable_context sechyps) in
   List.rev_map (Libnames.make_path dir) args
 
 let discharge_constant ((sp, kn), obj) =
-  let con = constant_of_kn kn in
+  let con = Constant.make1 kn in
   let from = Global.lookup_constant con in
   let modlist = replacement_context () in
   let hyps,subst,uctx = section_segment_of_constant con in
@@ -311,9 +311,9 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists (List.map fst names);
   let id = basename sp in
-  let _,dir,_ = repr_kn kn in
+  let _,dir,_ = KerName.repr kn in
   let kn' = Global.add_mind dir id mie in
-  assert (eq_mind kn' (mind_of_kn kn));
+  assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
   add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
@@ -384,7 +384,7 @@ let declare_projections mind =
 	let kn' = declare_constant id (ProjectionEntry entry,
 				       IsDefinition StructureComponent)
 	in
-	  assert(eq_constant kn kn')) kns; true,true
+	  assert(Constant.equal kn kn')) kns; true,true
     | Some None -> true,false
     | None -> false,false
 
diff --git a/interp/declare.mli b/interp/declare.mli
index ccd7d28bb..86d33cfb2 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -52,17 +52,17 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   internal specify if the constant has been created by the kernel or by the
   user, and in the former case, if its errors should be silent *)
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
+ ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
-  constr Univ.in_universe_context_set -> constant
+  constr Univ.in_universe_context_set -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
-  (string -> (inductive * constant) array -> unit) -> unit
+  (string -> (inductive * Constant.t) array -> unit) -> unit
 
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 561b0078a..13ed65056 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -231,7 +231,7 @@ let add_glob ?loc ref =
     add_glob_gen ?loc sp lib_dp ty
 
 let mp_of_kn kn =
-  let mp,sec,l = Names.repr_kn kn in
+  let mp,sec,l = Names.KerName.repr kn in
     Names.MPdot (mp,l)
 
 let add_glob_kn ?loc kn =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index afcd7a2ed..f3ad50f28 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -23,11 +23,11 @@ val pause : unit -> unit
 val continue : unit -> unit
 
 val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
-val add_glob_kn : ?loc:Loc.t -> Names.kernel_name -> unit
+val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
 
 val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit
-val dump_moddef : ?loc:Loc.t -> Names.module_path -> string -> unit
-val dump_modref  : ?loc:Loc.t -> Names.module_path -> string -> unit
+val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
+val dump_modref  : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_reference  : ?loc:Loc.t -> string -> string -> string -> unit
 val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 09a0ba83c..daec1191e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -483,8 +483,8 @@ type implicit_interactive_request =
 
 type implicit_discharge_request =
   | ImplLocal
-  | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of mutual_inductive * implicits_flags
+  | ImplConstant of Constant.t * implicits_flags
+  | ImplMutualInductive of MutInd.t * implicits_flags
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 4b78f54ea..658d9e01a 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -98,8 +98,8 @@ val compute_implicits_names : env -> types -> Name.t list
 (** {6 Computation of implicits (done using the global environment). } *)
 
 val declare_var_implicits : variable -> unit
-val declare_constant_implicits : constant -> unit
-val declare_mib_implicits : mutual_inductive -> unit
+val declare_constant_implicits : Constant.t -> unit
+val declare_mib_implicits : MutInd.t -> unit
 
 val declare_implicits : bool -> global_reference -> unit
 
diff --git a/interp/notation.ml b/interp/notation.ml
index d3cac1e3e..076570c8a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -234,7 +234,7 @@ let find_delimiters_scope ?loc key =
 
 type interp_rule =
   | NotationRule of scope_name option * notation
-  | SynDefRule of kernel_name
+  | SynDefRule of KerName.t
 
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 75c8d5aa5..e312a3767 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -110,7 +110,7 @@ val availability_of_prim_token :
 (** Binds a notation in a given scope to an interpretation *)
 type interp_rule =
   | NotationRule of scope_name option * notation
-  | SynDefRule of kernel_name
+  | SynDefRule of KerName.t
 
 val declare_notation_interpretation : notation -> scope_name option ->
       interpretation -> notation_location -> onlyprint:bool -> unit
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 36a3986b5..4d2cb5b74 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -16,4 +16,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 val declare_syntactic_definition : bool -> Id.t ->
   Flags.compat_version option -> syndef_interpretation -> unit
 
-val search_syntactic_definition : kernel_name -> syndef_interpretation
+val search_syntactic_definition : KerName.t -> syndef_interpretation
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 7e193ef82..e8cce0841 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -85,7 +85,7 @@ module type RedFlagsSig = sig
   val fFIX : red_kind
   val fCOFIX : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
+  val fCONST : Constant.t -> red_kind
   val fVAR : Id.t -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
@@ -114,7 +114,7 @@ module RedFlags = (struct
 
   type red_kind = BETA | DELTA | ETA | MATCH | FIX
               | COFIX | ZETA
-	      | CONST of constant | VAR of Id.t
+	      | CONST of Constant.t | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fETA = ETA
@@ -234,7 +234,7 @@ let unfold_red kn =
  * instantiations (cbv or lazy) are.
  *)
 
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 let eq_pconstant_key (c,u) (c',u') =
   eq_constant_key c c' && Univ.Instance.equal u u'
@@ -401,7 +401,7 @@ let update v1 no t =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * Constant.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9e5cb48a4..de1bb120e 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -29,7 +29,7 @@ val all_opaque      : transparent_state
 val all_transparent : transparent_state
 
 val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> constant -> bool
+val is_transparent_constant : transparent_state -> Constant.t -> bool
 
 (** Sets of reduction kinds. *)
 module type RedFlagsSig = sig
@@ -46,7 +46,7 @@ module type RedFlagsSig = sig
   val fFIX : red_kind
   val fCOFIX : red_kind
   val fZETA : red_kind
-  val fCONST : constant -> red_kind
+  val fCONST : Constant.t -> red_kind
   val fVAR : Id.t -> red_kind
 
   (** No reduction at all *)
@@ -92,7 +92,7 @@ val unfold_side_red : reds
 val unfold_red : evaluable_global_reference -> reds
 
 (***********************************************************************)
-type table_key = constant puniverses tableKey
+type table_key = Constant.t puniverses tableKey
 
 type 'a infos_cache
 type 'a infos = {
@@ -145,7 +145,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * Constant.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 25f61c7aa..63b0e6929 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -74,7 +74,7 @@ type instruction =
   | Kclosurerec of int * int * Label.t array * Label.t array
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (* nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of constant
+  | Kgetglobal of Constant.t
   | Kconst of structured_constant
   | Kmakeblock of int * tag
   | Kmakeprod
@@ -193,7 +193,7 @@ let pp_sort s =
 
 let rec pp_struct_const = function
   | Const_sorts s -> pp_sort s
-  | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i
+  | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i
   | Const_proj p -> Constant.print p
   | Const_b0 i -> int i
   | Const_bn (i,t) ->
@@ -241,7 +241,7 @@ let rec pp_instr i =
 	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
 	     str " bodies = " ++
 	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
-  | Kgetglobal idu -> str "getglobal " ++ pr_con idu
+  | Kgetglobal idu -> str "getglobal " ++ Constant.print idu
   | Kconst sc ->
       str "const " ++ pp_struct_const sc
   | Kmakeblock(n, m) ->
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 718917ab3..e9070b26a 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -69,7 +69,7 @@ type instruction =
                    (** nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (** nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of constant
+  | Kgetglobal of Constant.t
   | Kconst of structured_constant
   | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
                                          ** is accu, all others are popped from
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d63fcffa2..5bac26bf9 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -998,7 +998,7 @@ let compile_constant_body fail_on_error env univs = function
       match kind_of_term body with
 	| Const (kn',u) when is_univ_copy instance_size u ->
 	    (* we use the canonical name of the constant*)
-	    let con= constant_of_kn (canonical_con kn') in
+	    let con= Constant.make1 (Constant.canonical kn') in
 	      Some (BCalias (get_alias env con))
 	| _ ->
 	    let res = compile fail_on_error ~universes:instance_size env body in
@@ -1006,7 +1006,7 @@ let compile_constant_body fail_on_error env univs = function
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias kn = BCalias (constant_of_kn (canonical_con kn))
+let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn))
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 48c2e4533..9209e8460 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -14,7 +14,7 @@ val compile_constant_body : bool ->
 
 (** Shortcut of the previous function used during module strengthening *)
 
-val compile_alias : Names.constant -> body_code
+val compile_alias : Names.Constant.t -> body_code
 
 (** spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 092bcecc3..eeea19c12 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -19,7 +19,7 @@ open Mod_subst
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of Names.constant
+  | Reloc_getglobal of Names.Constant.t
 
 type patch = reloc_info * int
 
@@ -348,12 +348,12 @@ let subst_to_patch s (code,pl,fv) =
 
 type body_code =
   | BCdefined of to_patch
-  | BCalias of Names.constant
+  | BCalias of Names.Constant.t
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCalias of Names.constant substituted
+| PBCalias of Names.Constant.t substituted
 | PBCconstant
 
 let from_val = function
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index c80edd596..fee45aafd 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant
+  | Reloc_getglobal of Constant.t
 
 type patch = reloc_info * int
 
@@ -23,7 +23,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCalias of constant
+  | BCalias of Constant.t
   | BCconstant
 
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c3e609536..cec00c04b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -75,7 +75,7 @@ type ('constr, 'types) pfixpoint =
 type ('constr, 'types) pcofixpoint =
     int * ('constr, 'types) prec_declaration
 type 'a puniverses = 'a Univ.puniverses
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of (constant * 'univs)
+  | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
@@ -520,7 +520,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
         eq c1 c2 && Array.equal_norefl eq l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
-  | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
+  | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2
   | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
   | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
@@ -681,7 +681,7 @@ let constr_ord_int f t1 t2 =
     | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
     | Evar (e1,l1), Evar (e2,l2) ->
         (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
-    | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2
+    | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2
     | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2
     | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 76dbf5530..da074d85c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -15,7 +15,7 @@ open Names
 type 'a puniverses = 'a Univ.puniverses
 
 (** {6 Simply type aliases } *)
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -113,8 +113,8 @@ val mkApp : constr * constr array -> constr
 
 val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
 
-(** Constructs a constant *)
-val mkConst : constant -> constr
+(** Constructs a Constant.t *)
+val mkConst : Constant.t -> constr
 val mkConstU : pconstant -> constr
 
 (** Constructs a projection application *)
@@ -208,7 +208,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
                                                           - [F] itself is not {!App}
                                                           - and [[|P1;..;Pn|]] is not empty. *)
 
-  | Const     of (constant * 'univs)                  (** Gallina-variable that was introduced by Vernacular-command that extends the global environment
+  | Const     of (Constant.t * 'univs)                  (** Gallina-variable that was introduced by Vernacular-command that extends the global environment
                                                           (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *)
 
   | Ind       of (inductive * 'univs)                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
@@ -302,7 +302,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
 
 (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances (the first boolean tells if they belong to a constant), [s] to 
+   instances (the first boolean tells if they belong to a Constant.t), [s] to 
    compare sorts; Cast's, binders name and Cases annotations are not taken 
     into account *)
 
@@ -335,7 +335,7 @@ val compare_head_gen_with :
 (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
     [f] to compare the immediate subterms of [c1] of [c2] for
     conversion, [fle] for cumulativity, [u] to compare universe
-    instances (the first boolean tells if they belong to a constant),
+    instances (the first boolean tells if they belong to a Constant.t),
     [s] to compare sorts for for subtyping; Cast's, binders name and
     Cases annotations are not taken into account *)
 
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 248cd2b30..02c179ab6 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -16,7 +16,7 @@ val empty : oracle
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : ('a -> constant) -> oracle -> bool -> 
+val oracle_order : ('a -> Constant.t) -> oracle -> bool -> 
   'a tableKey -> 'a tableKey -> bool
 
 (** Priority for the expansion of constant in the conversion test.
@@ -30,14 +30,14 @@ val transparent : level
 (** Check whether a level is transparent *)
 val is_transparent : level -> bool
 
-val get_strategy : oracle -> constant tableKey -> level
+val get_strategy : oracle -> Constant.t tableKey -> level
 
 (** Sets the level of a constant.
  * Level of RelKey constant cannot be set. *)
-val set_strategy : oracle -> constant tableKey -> level -> oracle
+val set_strategy : oracle -> Constant.t tableKey -> level -> oracle
 
 (** Fold over the non-transparent levels of the oracle. Order unspecified. *)
-val fold_strategy : (constant tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
+val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
 
 val get_transp_state : oracle -> transparent_state
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 80d41847c..08fff0ca4 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -29,15 +29,15 @@ let pop_dirpath p = match DirPath.repr p with
   | _::l -> DirPath.make l
 
 let pop_mind kn =
-  let (mp,dir,l) = Names.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_con con =
-  let (mp,dir,l) = Names.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
 
 type my_global_reference =
-  | ConstRef of constant
+  | ConstRef of Constant.t
   | IndRef of inductive
   | ConstructRef of constructor
 
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 633cf0abd..30d0e5588 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -14,5 +14,5 @@ open Pre_env
 
 val val_of_constr : env -> constr -> values
 
-val set_opaque_const      : constant -> unit
-val set_transparent_const : constant -> unit
+val set_opaque_const      : Constant.t -> unit
+val set_transparent_const : Constant.t -> unit
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index e17fb1c38..8b949f928 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -48,7 +48,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : mutual_inductive;
+  proj_ind : MutInd.t;
   proj_npars : int;
   proj_arg : int;
   proj_type : types; (* Type under params *)
@@ -115,7 +115,7 @@ v}
     - The constants associated to each projection.
     - The checked projection bodies. *)
 
-type record_body = (Id.t * constant array * projection_body array) option
+type record_body = (Id.t * Constant.t array * projection_body array) option
 
 type regular_inductive_arity = {
   mind_user_arity : types;
@@ -212,12 +212,12 @@ type ('ty,'a) functorize =
     only for short module printing and for extraction. *)
 
 type with_declaration =
-  | WithMod of Id.t list * module_path
+  | WithMod of Id.t list * ModPath.t
   | WithDef of Id.t list * constr Univ.in_universe_context
 
 type module_alg_expr =
-  | MEident of module_path
-  | MEapply of module_alg_expr * module_path
+  | MEident of ModPath.t
+  | MEapply of module_alg_expr * ModPath.t
   | MEwith of module_alg_expr * with_declaration
 
 (** A component of a module structure *)
@@ -251,7 +251,7 @@ and module_implementation =
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 and 'a generic_module_body =
-  { mod_mp : module_path; (** absolute path of the module *)
+  { mod_mp : ModPath.t; (** absolute path of the module *)
     mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
@@ -290,5 +290,5 @@ and _ module_retroknowledge =
 
     - A module application is atomic, for instance ((M N) P) :
       * the head of [MEapply] can only be another [MEapply] or a [MEident]
-      * the argument of [MEapply] is now directly forced to be a [module_path].
+      * the argument of [MEapply] is now directly forced to be a [ModPath.t].
 *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 66d66c7d0..d7329a319 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -287,9 +287,9 @@ let hcons_mind mib =
 (** {6 Stm machinery } *)
 
 let string_of_side_effect { Entries.eff } = match eff with
-  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
+  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")"
   | Entries.SEscheme (cl,_) ->
-      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
+      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")"
 
 (** Hashconsing of modules *)
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index a1ccbdbc1..f294c4ce4 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -85,7 +85,7 @@ type parameter_entry =
     Context.Named.t option * bool * types Univ.in_universe_context * inline 
 
 type projection_entry = {
-  proj_entry_ind : mutual_inductive;
+  proj_entry_ind : MutInd.t;
   proj_entry_arg : int }
 
 type 'a constant_entry =
@@ -115,8 +115,8 @@ type seff_env =
   | `Opaque of Constr.t * Univ.universe_context_set ]
 
 type side_eff =
-  | SEsubproof of constant * Declarations.constant_body * seff_env
-  | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
+  | SEsubproof of Constant.t * Declarations.constant_body * seff_env
+  | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string
 
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2667ad7ca..37816f1e5 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -126,19 +126,19 @@ val pop_rel_context : int -> env -> env
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
-val add_constant : constant -> constant_body -> env -> env
-val add_constant_key : constant -> constant_body -> Pre_env.link_info ->
+val add_constant : Constant.t -> constant_body -> env -> env
+val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info ->
   env -> env
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
-val lookup_constant    : constant -> env -> constant_body
-val evaluable_constant : constant -> env -> bool
+val lookup_constant    : Constant.t -> env -> constant_body
+val evaluable_constant : Constant.t -> env -> bool
 
 (** New-style polymorphism *)
-val polymorphic_constant  : constant -> env -> bool
+val polymorphic_constant  : Constant.t -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
-val type_in_type_constant : constant -> env -> bool
+val type_in_type_constant : Constant.t -> env -> bool
 
 (** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
@@ -149,35 +149,35 @@ val type_in_type_constant : constant -> env -> bool
 type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 
-val constant_value : env -> constant puniverses -> constr constrained
-val constant_type : env -> constant puniverses -> types constrained
+val constant_value : env -> Constant.t puniverses -> constr constrained
+val constant_type : env -> Constant.t puniverses -> types constrained
 
-val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
-val constant_value_and_type : env -> constant puniverses -> 
+val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option
+val constant_value_and_type : env -> Constant.t puniverses -> 
   constr option * types * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
-val constant_context : env -> constant -> Univ.abstract_universe_context
+val constant_context : env -> Constant.t -> Univ.abstract_universe_context
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
-val constant_value_in : env -> constant puniverses -> constr
-val constant_type_in : env -> constant puniverses -> types
-val constant_opt_value_in : env -> constant puniverses -> constr option
+val constant_value_in : env -> Constant.t puniverses -> constr
+val constant_type_in : env -> Constant.t puniverses -> types
+val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 (** {6 Primitive projections} *)
 
 val lookup_projection    : Names.projection -> env -> projection_body
-val is_projection : constant -> env -> bool
+val is_projection : Constant.t -> env -> bool
 
 (** {5 Inductive types } *)
-val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env
-val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
+val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env
+val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
 
 (** Looks up in the context of global inductive names 
    raises [Not_found] if the required path is not found *)
-val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
+val lookup_mind : MutInd.t -> env -> mutual_inductive_body
 
 (** New-style polymorphism *)
 val polymorphic_ind  : inductive -> env -> bool
@@ -195,8 +195,8 @@ val add_modtype : module_type_body -> env -> env
 (** [shallow_add_module] does not add module components *)
 val shallow_add_module : module_body -> env -> env
 
-val lookup_module : module_path -> env -> module_body
-val lookup_modtype : module_path -> env -> module_type_body
+val lookup_module : ModPath.t -> env -> module_body
+val lookup_modtype : ModPath.t -> env -> module_type_body
 
 (** {5 Universe constraints } *)
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e248436ec..c0f564dc3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -787,7 +787,7 @@ exception UndefinableExpansion
     a substitution of the form [params, x : ind params] *)
 let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     mind_consnrealdecls mind_consnrealargs paramslet ctx =
-  let mp, dp, l = repr_mind kn in
+  let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index e4b7c086a..f5d0ed3f2 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -34,7 +34,7 @@ exception InductiveError of inductive_error
 
 (** The following function does checks on inductive declarations. *)
 
-val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
+val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
 (** The following enforces a system compatible with the univalent model *)
 
@@ -44,4 +44,4 @@ val is_indices_matter : unit -> bool
 val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.Rel.t -> int array -> int array -> 
   Context.Rel.t -> Context.Rel.t -> 
-  (constant array * projection_body array)
+  (Constant.t array * projection_body array)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 0dfa8db00..1caede857 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -32,7 +32,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 val lookup_mind_specif : env -> inductive -> mind_specif
 
 (** {6 Functions to build standard types related to inductive } *)
-val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
+val ind_subst : MutInd.t -> mutual_inductive_body -> universe_instance -> constr list
 
 val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
 
@@ -65,7 +65,7 @@ val arities_of_constructors : pinductive -> mind_specif -> types array
 val type_of_constructors : pinductive -> mind_specif -> types array
 
 (** Transforms inductive specification into types (in nf) *)
-val arities_of_specif : mutual_inductive puniverses -> mind_specif -> types array
+val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array
 
 val inductive_params : mind_specif -> int
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 7b660939b..1793e4f71 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -23,13 +23,13 @@ open Term
 
 type delta_hint =
   | Inline of int * constr option
-  | Equiv of kernel_name
+  | Equiv of KerName.t
 
-(* NB: earlier constructor Prefix_equiv of module_path
+(* NB: earlier constructor Prefix_equiv of ModPath.t
    is now stored in a separate table, see Deltamap.t below *)
 
 module Deltamap = struct
-  type t = module_path MPmap.t * delta_hint KNmap.t
+  type t = ModPath.t MPmap.t * delta_hint KNmap.t
   let empty = MPmap.empty, KNmap.empty
   let is_empty (mm, km) =
     MPmap.is_empty mm && KNmap.is_empty km
@@ -45,7 +45,7 @@ module Deltamap = struct
 end
 
 (* Invariant: in the [delta_hint] map, an [Equiv] should only
-   relate [kernel_name] with the same label (and section dirpath). *)
+   relate [KerName.t] with the same label (and section dirpath). *)
 
 type delta_resolver = Deltamap.t
 
@@ -65,7 +65,7 @@ module Umap = struct
   let join map1 map2 = fold add_mp add_mbi map1 map2
 end
 
-type substitution = (module_path * delta_resolver) Umap.t
+type substitution = (ModPath.t * delta_resolver) Umap.t
 
 let empty_subst = Umap.empty
 
@@ -76,21 +76,21 @@ let is_empty_subst = Umap.is_empty
 let string_of_hint = function
   | Inline (_,Some _) -> "inline(Some _)"
   | Inline _ -> "inline()"
-  | Equiv kn -> string_of_kn kn
+  | Equiv kn -> KerName.to_string kn
 
 let debug_string_of_delta resolve =
   let kn_to_string kn hint l =
-    (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l
+    (KerName.to_string kn ^ "=>" ^ string_of_hint hint) :: l
   in
   let mp_to_string mp mp' l =
-    (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l
+    (ModPath.to_string mp ^ "=>" ^ ModPath.to_string mp') :: l
   in
   let l = Deltamap.fold mp_to_string kn_to_string resolve [] in
   String.concat ", " (List.rev l)
 
 let list_contents sub =
-  let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
-  let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in
+  let one_pair (mp,reso) = (ModPath.to_string mp,debug_string_of_delta reso) in
+  let mp_one_pair mp0 p l = (ModPath.to_string mp0, one_pair p)::l in
   let mbi_one_pair mbi p l = (MBId.debug_to_string mbi, one_pair p)::l in
   Umap.fold mp_one_pair mbi_one_pair sub []
 
@@ -117,7 +117,7 @@ let debug_pr_subst sub =
 let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc))
 
 let add_kn_delta_resolver kn kn' =
-  assert (Label.equal (label kn) (label kn'));
+  assert (Label.equal (KerName.label kn) (KerName.label kn'));
   Deltamap.add_kn kn (Equiv kn')
 
 let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
@@ -165,12 +165,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 = repr_kn kn in
+    let mp,dir,l = KerName.repr kn in
     let new_mp = find_prefix resolve mp in
     if mp == new_mp then
       kn
     else
-      make_kn new_mp dir l
+      KerName.make new_mp dir l
 
 let kn_of_delta resolve kn =
   try solve_delta_kn resolve kn
@@ -242,18 +242,18 @@ let subst_mp sub mp =
   | Some (mp',_) -> mp'
 
 let subst_kn_delta sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',resolve) ->
-      solve_delta_kn resolve (make_kn mp' dir l)
+      solve_delta_kn resolve (KerName.make mp' dir l)
    | None -> kn
 
 
 let subst_kn sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      (make_kn mp' dir l)
+      (KerName.make mp' dir l)
    | None -> kn
 
 exception No_subst
@@ -419,7 +419,7 @@ let subst_mps sub c =
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
-    | _ when mp_eq mp mpfrom -> mpto
+    | _ when ModPath.equal mp mpfrom -> mpto
     | MPdot (mp1,l) ->
 	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
 	  if mp1 == mp1' then mp
@@ -427,14 +427,14 @@ let rec replace_mp_in_mp mpfrom mpto mp =
     | _ -> mp
 
 let replace_mp_in_kn mpfrom mpto kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
   let mp'' = replace_mp_in_mp mpfrom mpto mp in
     if mp==mp'' then kn
-    else make_kn mp'' dir l
+    else KerName.make mp'' dir l
 
 let rec mp_in_mp mp mp1 =
   match mp1 with
-    | _ when mp_eq mp1 mp -> true
+    | _ when ModPath.equal mp1 mp -> true
     | MPdot (mp2,l) -> mp_in_mp mp mp2
     | _ -> false
 
@@ -446,7 +446,7 @@ let subset_prefixed_by mp resolver =
     match hint with
       | Inline _ -> rslv
       | Equiv _ ->
-	if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
+	if mp_in_mp mp (KerName.modpath kn) then Deltamap.add_kn kn hint rslv else rslv
   in
   Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
 
@@ -515,7 +515,7 @@ let add_delta_resolver resolver1 resolver2 =
 
 let substition_prefixed_by k mp subst =
   let mp_prefixmp kmp (mp_to,reso) sub =
-    if mp_in_mp mp kmp && not (mp_eq mp kmp) then
+    if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then
       let new_key = replace_mp_in_mp mp k kmp in
       Umap.add_mp new_key (mp_to,reso) sub
     else sub
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index f1d0e4279..1d7012ce5 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -20,44 +20,44 @@ type delta_resolver
 val empty_delta_resolver : delta_resolver
 
 val add_mp_delta_resolver :
-  module_path -> module_path -> delta_resolver -> delta_resolver
+  ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver
 
 val add_kn_delta_resolver :
-  kernel_name -> kernel_name -> delta_resolver -> delta_resolver
+  KerName.t -> KerName.t -> delta_resolver -> delta_resolver
 
 val add_inline_delta_resolver :
-  kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver
+  KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
 (** Effect of a [delta_resolver] on a module path, on a kernel name *)
 
-val mp_of_delta : delta_resolver -> module_path -> module_path
-val kn_of_delta : delta_resolver -> kernel_name -> kernel_name
+val mp_of_delta : delta_resolver -> ModPath.t -> ModPath.t
+val kn_of_delta : delta_resolver -> KerName.t -> KerName.t
 
 (** Build a constant whose canonical part is obtained via a resolver *)
 
-val constant_of_delta_kn : delta_resolver -> kernel_name -> constant
+val constant_of_delta_kn : delta_resolver -> KerName.t -> Constant.t
 
 (** Same, but a 2nd resolver is tried if the 1st one had no effect *)
 
 val constant_of_deltas_kn :
-  delta_resolver -> delta_resolver -> kernel_name -> constant
+  delta_resolver -> delta_resolver -> KerName.t -> Constant.t
 
 (** Same for inductive names *)
 
-val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive
+val mind_of_delta_kn : delta_resolver -> KerName.t -> MutInd.t
 val mind_of_deltas_kn :
-  delta_resolver -> delta_resolver -> kernel_name -> mutual_inductive
+  delta_resolver -> delta_resolver -> KerName.t -> MutInd.t
 
 (** Extract the set of inlined constant in the resolver *)
-val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list
+val inline_of_delta : int option -> delta_resolver -> (int * KerName.t) list
 
 (** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *)
 
-val mp_in_delta : module_path -> delta_resolver -> bool
-val con_in_delta : constant -> delta_resolver -> bool
-val mind_in_delta : mutual_inductive -> delta_resolver -> bool
+val mp_in_delta : ModPath.t -> delta_resolver -> bool
+val con_in_delta : Constant.t -> delta_resolver -> bool
+val mind_in_delta : MutInd.t -> delta_resolver -> bool
 
 
 (** {6 Substitution} *)
@@ -72,15 +72,15 @@ val is_empty_subst : substitution -> bool
    composition. Most often this is not what you want. For sequential
    composition, try [join (map_mbid mp delta) subs] **)
 val add_mbid :
-  MBId.t -> module_path -> delta_resolver  -> substitution -> substitution
+  MBId.t -> ModPath.t -> delta_resolver  -> substitution -> substitution
 val add_mp :
-  module_path -> module_path -> delta_resolver -> substitution -> substitution
+  ModPath.t -> ModPath.t -> delta_resolver -> substitution -> substitution
 
 (** map_* create a new substitution [arg2/arg1]\{arg3\} *)
 val map_mbid :
-  MBId.t -> module_path -> delta_resolver -> substitution
+  MBId.t -> ModPath.t -> delta_resolver -> substitution
 val map_mp :
-  module_path -> module_path -> delta_resolver -> substitution
+  ModPath.t -> ModPath.t -> delta_resolver -> substitution
 
 (** sequential composition:
    [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
@@ -117,10 +117,10 @@ val debug_pr_delta : delta_resolver -> Pp.t
    as well [==] *)
 
 val subst_mp :
-  substitution -> module_path -> module_path
+  substitution -> ModPath.t -> ModPath.t
 
 val subst_mind :
-  substitution -> mutual_inductive -> mutual_inductive
+  substitution -> MutInd.t -> MutInd.t
 
 val subst_ind :
   substitution -> inductive -> inductive
@@ -128,10 +128,10 @@ val subst_ind :
 val subst_pind : substitution -> pinductive -> pinductive
 
 val subst_kn :
-  substitution -> kernel_name -> kernel_name
+  substitution -> KerName.t -> KerName.t
 
 val subst_con :
-  substitution -> pconstant -> constant * constr
+  substitution -> pconstant -> Constant.t * constr
 
 val subst_pcon :
   substitution -> pconstant -> pconstant
@@ -140,10 +140,10 @@ val subst_pcon_term :
   substitution -> pconstant -> pconstant * constr
 
 val subst_con_kn :
-  substitution -> constant -> constant * constr
+  substitution -> Constant.t -> Constant.t * constr
 
-val subst_constant : 
-  substitution -> constant -> constant
+val subst_constant :
+  substitution -> Constant.t -> Constant.t
 
 (** Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
@@ -154,7 +154,7 @@ val subst_evaluable_reference :
   substitution -> evaluable_global_reference -> evaluable_global_reference
 
 (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
-val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name
+val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
 
 (** [subst_mps sub c] performs the substitution [sub] on all kernel
    names appearing in [c] *)
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index dcabb1334..1225c3e1e 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -21,16 +21,16 @@ open Names
 *)
 
 val translate_module :
-  env -> module_path -> inline -> module_entry -> module_body
+  env -> ModPath.t -> inline -> module_entry -> module_body
 
 (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
     cannot be [None] (and of course [mod_expr] is [Abstract]). *)
 
 val translate_modtype :
-  env -> module_path -> inline -> module_type_entry -> module_type_body
+  env -> ModPath.t -> inline -> module_type_entry -> module_type_body
 
 (** Low-level function for translating a module struct entry :
-    - We translate to a module when a [module_path] is given,
+    - We translate to a module when a [ModPath.t] is given,
       otherwise to a module type.
     - The first output is the expanded signature
     - The second output is the algebraic expression, kept mostly for
@@ -40,14 +40,14 @@ type 'alg translation =
   module_signature * 'alg * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
-  env -> module_path option -> inline -> module_struct_entry ->
+  env -> ModPath.t option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
 (** From an already-translated (or interactive) implementation and
     an (optional) signature entry, produces a final [module_body] *)
 
 val finalize_module :
-  env -> module_path -> (module_expression option) translation ->
+  env -> ModPath.t -> (module_expression option) translation ->
   (module_type_entry * inline) option ->
   module_body
 
@@ -55,5 +55,5 @@ val finalize_module :
     module type given to an Include *)
 
 val translate_mse_incl :
-  bool -> env -> module_path -> inline -> module_struct_entry ->
+  bool -> env -> ModPath.t -> inline -> module_struct_entry ->
     unit translation
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 76915e917..c10af0725 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -59,7 +59,7 @@ type module_typing_error =
   | NotAFunctor
   | IsAFunctor
   | IncompatibleModuleTypes of module_type_body * module_type_body
-  | NotEqualModulePaths of module_path * module_path
+  | NotEqualModulePaths of ModPath.t * ModPath.t
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
   | NotAModule of string
@@ -68,7 +68,7 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
-  | IncludeRestrictedFunctor of module_path
+  | IncludeRestrictedFunctor of ModPath.t
 
 exception ModuleTypingError of module_typing_error
 
@@ -403,8 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	      let constr = Mod_subst.force_constr body in
 	      add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
-	  error_no_such_label_sub (con_label con)
-	    (string_of_mp (con_modpath con))
+	  error_no_such_label_sub (Constant.label con)
+	    (ModPath.to_string (Constant.modpath con))
   in
   make_inline delta constants
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e2a94b691..e1bba21d3 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -26,9 +26,9 @@ val destr_nofunctor : ('ty,'a) functorize -> 'a
 (** Conversions between [module_body] and [module_type_body] *)
 
 val module_type_of_module : module_body -> module_type_body
-val module_body_of_type : module_path -> module_type_body -> module_body
+val module_body_of_type : ModPath.t -> module_type_body -> module_body
 
-val check_modpath_equiv : env -> module_path -> module_path -> unit
+val check_modpath_equiv : env -> ModPath.t -> ModPath.t -> unit
 
 val implem_smartmap :
   (module_signature -> module_signature) ->
@@ -43,7 +43,7 @@ val subst_structure : substitution -> structure_body -> structure_body
 (** {6 Adding to an environment } *)
 
 val add_structure :
-  module_path -> structure_body -> delta_resolver -> env -> env
+  ModPath.t -> structure_body -> delta_resolver -> env -> env
 
 (** adds a module and its components, but not the constraints *)
 val add_module : module_body -> env -> env
@@ -53,19 +53,19 @@ the native compiler. The linking information is updated. *)
 val add_linked_module : module_body -> Pre_env.link_info -> env -> env
 
 (** same, for a module type *)
-val add_module_type : module_path -> module_type_body -> env -> env
+val add_module_type : ModPath.t -> module_type_body -> env -> env
 
 (** {6 Strengthening } *)
 
-val strengthen : module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> ModPath.t -> module_type_body
 
 val inline_delta_resolver :
-  env -> inline -> module_path -> MBId.t -> module_type_body ->
+  env -> inline -> ModPath.t -> MBId.t -> module_type_body ->
   delta_resolver -> delta_resolver
 
-val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
+val strengthen_and_subst_mb : module_body -> ModPath.t -> bool -> module_body
 
-val subst_modtype_and_resolver : module_type_body -> module_path ->
+val subst_modtype_and_resolver : module_type_body -> ModPath.t ->
   module_type_body
 
 (** {6 Cleaning a module expression from bounded parts }
@@ -118,7 +118,7 @@ type module_typing_error =
   | NotAFunctor
   | IsAFunctor
   | IncompatibleModuleTypes of module_type_body * module_type_body
-  | NotEqualModulePaths of module_path * module_path
+  | NotEqualModulePaths of ModPath.t * ModPath.t
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
   | NotAModule of string
@@ -127,7 +127,7 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
-  | IncludeRestrictedFunctor of module_path
+  | IncludeRestrictedFunctor of ModPath.t
 
 exception ModuleTypingError of module_typing_error
 
@@ -153,4 +153,4 @@ val error_generative_module_expected : Label.t -> 'a
 
 val error_no_such_label_sub : Label.t->string->'a
 
-val error_include_restricted_functor : module_path -> 'a
+val error_include_restricted_functor : ModPath.t -> 'a
diff --git a/kernel/names.mli b/kernel/names.mli
index d97fd2b3a..531a0cccb 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -113,6 +113,8 @@ end
 (** {6 Type aliases} *)
 
 type name = Name.t = Anonymous | Name of Id.t
+[@@ocaml.deprecated "Use Name.t"]
+
 type variable = Id.t
 type module_ident = Id.t
 
@@ -572,54 +574,55 @@ module Idmap : module type of Id.Map
 (** {5 Directory paths} *)
 
 type dir_path = DirPath.t
-(** @deprecated Alias for [DirPath.t]. *)
+[@@ocaml.deprecated "Alias for [DirPath.t]."]
 
-val dir_path_ord : dir_path -> dir_path -> int
-(** @deprecated Same as [DirPath.compare]. *)
+val dir_path_ord : DirPath.t -> DirPath.t -> int
+[@@ocaml.deprecated "Same as [DirPath.compare]."]
 
-val dir_path_eq : dir_path -> dir_path -> bool
-(** @deprecated Same as [DirPath.equal]. *)
+val dir_path_eq : DirPath.t -> DirPath.t -> bool
+[@@ocaml.deprecated "Same as [DirPath.equal]."]
 
-val make_dirpath : module_ident list -> dir_path
-(** @deprecated Same as [DirPath.make]. *)
+val make_dirpath : module_ident list -> DirPath.t
+[@@ocaml.deprecated "Same as [DirPath.make]."]
 
-val repr_dirpath : dir_path -> module_ident list
-(** @deprecated Same as [DirPath.repr]. *)
+val repr_dirpath : DirPath.t -> module_ident list
+[@@ocaml.deprecated "Same as [DirPath.repr]."]
 
-val empty_dirpath : dir_path
-(** @deprecated Same as [DirPath.empty]. *)
+val empty_dirpath : DirPath.t
+[@@ocaml.deprecated "Same as [DirPath.empty]."]
 
-val is_empty_dirpath : dir_path -> bool
-(** @deprecated Same as [DirPath.is_empty]. *)
+val is_empty_dirpath : DirPath.t -> bool
+[@@ocaml.deprecated "Same as [DirPath.is_empty]."]
 
-val string_of_dirpath : dir_path -> string
-(** @deprecated Same as [DirPath.to_string]. *)
+val string_of_dirpath : DirPath.t -> string
+[@@ocaml.deprecated "Same as [DirPath.to_string]."]
 
 val initial_dir : DirPath.t
-(** @deprecated Same as [DirPath.initial]. *)
+[@@ocaml.deprecated "Same as [DirPath.initial]."]
 
 (** {5 Labels} *)
 
 type label = Label.t
+[@@ocaml.deprecated "Same as [Label.t]."]
 (** Alias type *)
 
-val mk_label : string -> label
-(** @deprecated Same as [Label.make]. *)
+val mk_label : string -> Label.t
+[@@ocaml.deprecated "Same as [Label.make]."]
 
-val string_of_label : label -> string
-(** @deprecated Same as [Label.to_string]. *)
+val string_of_label : Label.t -> string
+[@@ocaml.deprecated "Same as [Label.to_string]."]
 
-val pr_label : label -> Pp.t
-(** @deprecated Same as [Label.print]. *)
+val pr_label : Label.t -> Pp.t
+[@@ocaml.deprecated "Same as [Label.print]."]
 
-val label_of_id : Id.t -> label
-(** @deprecated Same as [Label.of_id]. *)
+val label_of_id : Id.t -> Label.t
+[@@ocaml.deprecated "Same as [Label.of_id]."]
 
-val id_of_label : label -> Id.t
-(** @deprecated Same as [Label.to_id]. *)
+val id_of_label : Label.t -> Id.t
+[@@ocaml.deprecated "Same as [Label.to_id]."]
 
-val eq_label : label -> label -> bool
-(** @deprecated Same as [Label.equal]. *)
+val eq_label : Label.t -> Label.t -> bool
+[@@ocaml.deprecated "Same as [Label.equal]."]
 
 (** {5 Unique bound module names} *)
 
@@ -627,89 +630,89 @@ type mod_bound_id = MBId.t
 (** Alias type. *)
 
 val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
-(** @deprecated Same as [MBId.compare]. *)
+[@@ocaml.deprecated "Same as [MBId.compare]."]
 
 val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
-(** @deprecated Same as [MBId.equal]. *)
+[@@ocaml.deprecated "Same as [MBId.equal]."]
 
 val make_mbid : DirPath.t -> Id.t -> mod_bound_id
-(** @deprecated Same as [MBId.make]. *)
+[@@ocaml.deprecated "Same as [MBId.make]."]
 
 val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t
-(** @deprecated Same as [MBId.repr]. *)
+[@@ocaml.deprecated "Same as [MBId.repr]."]
 
 val id_of_mbid : mod_bound_id -> Id.t
-(** @deprecated Same as [MBId.to_id]. *)
+[@@ocaml.deprecated "Same as [MBId.to_id]."]
 
 val string_of_mbid : mod_bound_id -> string
-(** @deprecated Same as [MBId.to_string]. *)
+[@@ocaml.deprecated "Same as [MBId.to_string]."]
 
 val debug_string_of_mbid : mod_bound_id -> string
-(** @deprecated Same as [MBId.debug_to_string]. *)
+[@@ocaml.deprecated "Same as [MBId.debug_to_string]."]
 
 (** {5 Names} *)
 
-val name_eq : name -> name -> bool
-(** @deprecated Same as [Name.equal]. *)
+val name_eq : Name.t -> Name.t -> bool
+[@@ocaml.deprecated "Same as [Name.equal]."]
 
 (** {5 Module paths} *)
 
 type module_path = ModPath.t =
   | MPfile of DirPath.t
   | MPbound of MBId.t
-  | MPdot of module_path * Label.t
-(** @deprecated Alias type *)
+  | MPdot of ModPath.t * Label.t
+[@@ocaml.deprecated "Alias type"]
 
-val mp_ord : module_path -> module_path -> int
-(** @deprecated Same as [ModPath.compare]. *)
+val mp_ord : ModPath.t -> ModPath.t -> int
+[@@ocaml.deprecated "Same as [ModPath.compare]."]
 
-val mp_eq : module_path -> module_path -> bool
-(** @deprecated Same as [ModPath.equal]. *)
+val mp_eq : ModPath.t -> ModPath.t -> bool
+[@@ocaml.deprecated "Same as [ModPath.equal]."]
 
-val check_bound_mp : module_path -> bool
-(** @deprecated Same as [ModPath.is_bound]. *)
+val check_bound_mp : ModPath.t -> bool
+[@@ocaml.deprecated "Same as [ModPath.is_bound]."]
 
-val string_of_mp : module_path -> string
-(** @deprecated Same as [ModPath.to_string]. *)
+val string_of_mp : ModPath.t -> string
+[@@ocaml.deprecated "Same as [ModPath.to_string]."]
 
-val initial_path : module_path
-(** @deprecated Same as [ModPath.initial]. *)
+val initial_path : ModPath.t
+[@@ocaml.deprecated "Same as [ModPath.initial]."]
 
 (** {5 Kernel names} *)
 
 type kernel_name = KerName.t
-(** @deprecated Alias type *)
+[@@ocaml.deprecated "Alias type"]
 
-val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name
-(** @deprecated Same as [KerName.make]. *)
+val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t
+[@@ocaml.deprecated "Same as [KerName.make]."]
 
-val repr_kn : kernel_name -> module_path * DirPath.t * Label.t
-(** @deprecated Same as [KerName.repr]. *)
+val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t
+[@@ocaml.deprecated "Same as [KerName.repr]."]
 
-val modpath : kernel_name -> module_path
-(** @deprecated Same as [KerName.modpath]. *)
+val modpath : KerName.t -> ModPath.t
+[@@ocaml.deprecated "Same as [KerName.modpath]."]
 
-val label : kernel_name -> Label.t
-(** @deprecated Same as [KerName.label]. *)
+val label : KerName.t -> Label.t
+[@@ocaml.deprecated "Same as [KerName.label]."]
 
-val string_of_kn : kernel_name -> string
-(** @deprecated Same as [KerName.to_string]. *)
+val string_of_kn : KerName.t -> string
+[@@ocaml.deprecated "Same as [KerName.to_string]."]
 
-val pr_kn : kernel_name -> Pp.t
-(** @deprecated Same as [KerName.print]. *)
+val pr_kn : KerName.t -> Pp.t
+[@@ocaml.deprecated "Same as [KerName.print]."]
 
-val kn_ord : kernel_name -> kernel_name -> int
-(** @deprecated Same as [KerName.compare]. *)
+val kn_ord : KerName.t -> KerName.t -> int
+[@@ocaml.deprecated "Same as [KerName.compare]."]
 
 (** {5 Constant names} *)
 
 type constant = Constant.t
-(** @deprecated Alias type *)
+[@@ocaml.deprecated "Alias type"]
 
 module Projection : sig
   type t
-    
-  val make : constant -> bool -> t
+
+  val make : Constant.t -> bool -> t
 
   module SyntacticOrd : sig
     val compare : t -> t -> int
@@ -717,7 +720,7 @@ module Projection : sig
     val hash : t -> int
   end
 
-  val constant : t -> constant
+  val constant : t -> Constant.t
   val unfolded : t -> bool
   val unfold : t -> t
 
@@ -727,8 +730,8 @@ module Projection : sig
   (** Hashconsing of projections. *)
 
   val compare : t -> t -> int
-    
-  val map : (constant -> constant) -> t -> t
+
+  val map : (Constant.t -> Constant.t) -> t -> t
 
   val to_string : t -> string
   val print : t -> Pp.t
@@ -737,100 +740,100 @@ end
 
 type projection = Projection.t
 
-val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
-(** @deprecated Same as [Constant.make] *)
+val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
+[@@ocaml.deprecated "Same as [Constant.make]"]
 
-val constant_of_kn : KerName.t -> constant
-(** @deprecated Same as [Constant.make1] *)
+val constant_of_kn : KerName.t -> Constant.t
+[@@ocaml.deprecated "Same as [Constant.make1]"]
 
-val make_con : ModPath.t -> DirPath.t -> Label.t -> constant
-(** @deprecated Same as [Constant.make3] *)
+val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t
+[@@ocaml.deprecated "Same as [Constant.make3]"]
 
-val repr_con : constant -> ModPath.t * DirPath.t * Label.t
-(** @deprecated Same as [Constant.repr3] *)
+val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t
+[@@ocaml.deprecated "Same as [Constant.repr3]"]
 
-val user_con : constant -> KerName.t
-(** @deprecated Same as [Constant.user] *)
+val user_con : Constant.t -> KerName.t
+[@@ocaml.deprecated "Same as [Constant.user]"]
 
-val canonical_con : constant -> KerName.t
-(** @deprecated Same as [Constant.canonical] *)
+val canonical_con : Constant.t -> KerName.t
+[@@ocaml.deprecated "Same as [Constant.canonical]"]
 
-val con_modpath : constant -> ModPath.t
-(** @deprecated Same as [Constant.modpath] *)
+val con_modpath : Constant.t -> ModPath.t
+[@@ocaml.deprecated "Same as [Constant.modpath]"]
 
-val con_label : constant -> Label.t
-(** @deprecated Same as [Constant.label] *)
+val con_label : Constant.t -> Label.t
+[@@ocaml.deprecated "Same as [Constant.label]"]
 
-val eq_constant : constant -> constant -> bool
-(** @deprecated Same as [Constant.equal] *)
+val eq_constant : Constant.t -> Constant.t -> bool
+[@@ocaml.deprecated "Same as [Constant.equal]"]
 
-val con_ord : constant -> constant -> int
-(** @deprecated Same as [Constant.CanOrd.compare] *)
+val con_ord : Constant.t -> Constant.t -> int
+[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"]
 
-val con_user_ord : constant -> constant -> int
-(** @deprecated Same as [Constant.UserOrd.compare] *)
+val con_user_ord : Constant.t -> Constant.t -> int
+[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"]
 
-val con_with_label : constant -> Label.t -> constant
-(** @deprecated Same as [Constant.change_label] *)
+val con_with_label : Constant.t -> Label.t -> Constant.t
+[@@ocaml.deprecated "Same as [Constant.change_label]"]
 
-val string_of_con : constant -> string
-(** @deprecated Same as [Constant.to_string] *)
+val string_of_con : Constant.t -> string
+[@@ocaml.deprecated "Same as [Constant.to_string]"]
 
-val pr_con : constant -> Pp.t
-(** @deprecated Same as [Constant.print] *)
+val pr_con : Constant.t -> Pp.t
+[@@ocaml.deprecated "Same as [Constant.print]"]
 
-val debug_pr_con : constant -> Pp.t
-(** @deprecated Same as [Constant.debug_print] *)
+val debug_pr_con : Constant.t -> Pp.t
+[@@ocaml.deprecated "Same as [Constant.debug_print]"]
 
-val debug_string_of_con : constant -> string
-(** @deprecated Same as [Constant.debug_to_string] *)
+val debug_string_of_con : Constant.t -> string
+[@@ocaml.deprecated "Same as [Constant.debug_to_string]"]
 
 (** {5 Mutual Inductive names} *)
 
 type mutual_inductive = MutInd.t
-(** @deprecated Alias type *)
+[@@ocaml.deprecated "Alias type"]
 
-val mind_of_kn : KerName.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make1] *)
+val mind_of_kn : KerName.t -> MutInd.t
+[@@ocaml.deprecated "Same as [MutInd.make1]"]
 
-val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make] *)
+val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t
+[@@ocaml.deprecated "Same as [MutInd.make]"]
 
-val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make3] *)
+val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t
+[@@ocaml.deprecated "Same as [MutInd.make3]"]
 
-val user_mind : mutual_inductive -> KerName.t
-(** @deprecated Same as [MutInd.user] *)
+val user_mind : MutInd.t -> KerName.t
+[@@ocaml.deprecated "Same as [MutInd.user]"]
 
-val canonical_mind : mutual_inductive -> KerName.t
-(** @deprecated Same as [MutInd.canonical] *)
+val canonical_mind : MutInd.t -> KerName.t
+[@@ocaml.deprecated "Same as [MutInd.canonical]"]
 
-val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t
-(** @deprecated Same as [MutInd.repr3] *)
+val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t
+[@@ocaml.deprecated "Same as [MutInd.repr3]"]
 
-val eq_mind : mutual_inductive -> mutual_inductive -> bool
-(** @deprecated Same as [MutInd.equal] *)
+val eq_mind : MutInd.t -> MutInd.t -> bool
+[@@ocaml.deprecated "Same as [MutInd.equal]"]
 
-val mind_ord : mutual_inductive -> mutual_inductive -> int
-(** @deprecated Same as [MutInd.CanOrd.compare] *)
+val mind_ord : MutInd.t -> MutInd.t -> int
+[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"]
 
-val mind_user_ord : mutual_inductive -> mutual_inductive -> int
-(** @deprecated Same as [MutInd.UserOrd.compare] *)
+val mind_user_ord : MutInd.t -> MutInd.t -> int
+[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"]
 
-val mind_label : mutual_inductive -> Label.t
-(** @deprecated Same as [MutInd.label] *)
+val mind_label : MutInd.t -> Label.t
+[@@ocaml.deprecated "Same as [MutInd.label]"]
 
-val mind_modpath : mutual_inductive -> ModPath.t
-(** @deprecated Same as [MutInd.modpath] *)
+val mind_modpath : MutInd.t -> ModPath.t
+[@@ocaml.deprecated "Same as [MutInd.modpath]"]
 
-val string_of_mind : mutual_inductive -> string
-(** @deprecated Same as [MutInd.to_string] *)
+val string_of_mind : MutInd.t -> string
+[@@ocaml.deprecated "Same as [MutInd.to_string]"]
 
-val pr_mind : mutual_inductive -> Pp.t
-(** @deprecated Same as [MutInd.print] *)
+val pr_mind : MutInd.t -> Pp.t
+[@@ocaml.deprecated "Same as [MutInd.print]"]
 
-val debug_pr_mind : mutual_inductive -> Pp.t
-(** @deprecated Same as [MutInd.debug_print] *)
+val debug_pr_mind : MutInd.t -> Pp.t
+[@@ocaml.deprecated "Same as [MutInd.debug_print]"]
 
-val debug_string_of_mind : mutual_inductive -> string
-(** @deprecated Same as [MutInd.debug_to_string] *)
+val debug_string_of_mind : MutInd.t -> string
+[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"]
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 6e9991ac5..bb4c2585d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -25,7 +25,7 @@ to OCaml code. *)
 (** Local names **)
 
 (* The first component is there for debugging purposes only *)
-type lname = { lname : name; luid : int }
+type lname = { lname : Name.t; luid : int }
 
 let eq_lname ln1 ln2 =
   Int.equal ln1.luid ln2.luid
@@ -50,13 +50,13 @@ let fresh_lname n =
 type gname = 
   | Gind of string * inductive (* prefix, inductive name *)
   | Gconstruct of string * constructor (* prefix, constructor name *)
-  | Gconstant of string * constant (* prefix, constant name *)
-  | Gproj of string * constant (* prefix, constant name *)
-  | Gcase of label option * int
-  | Gpred of label option * int
-  | Gfixtype of label option * int
-  | Gnorm of label option * int
-  | Gnormtbl of label option * int
+  | Gconstant of string * Constant.t (* prefix, constant name *)
+  | Gproj of string * Constant.t (* prefix, constant name *)
+  | Gcase of Label.t option * int
+  | Gpred of Label.t option * int
+  | Gfixtype of Label.t option * int
+  | Gnorm of Label.t option * int
+  | Gnormtbl of Label.t option * int
   | Ginternal of string
   | Grel of int
   | Gnamed of Id.t
@@ -143,8 +143,8 @@ let fresh_gnormtbl l =
 type symbol =
   | SymbValue of Nativevalues.t
   | SymbSort of sorts
-  | SymbName of name
-  | SymbConst of constant
+  | SymbName of Name.t
+  | SymbConst of Constant.t
   | SymbMatch of annot_sw
   | SymbInd of inductive
   | SymbMeta of metavariable
@@ -296,7 +296,7 @@ type primitive =
   | MLmagic
   | MLarrayget
   | Mk_empty_instance
-  | Coq_primitive of CPrimitives.t * (prefix * constant) option
+  | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option
 
 let eq_primitive p1 p2 =
   match p1, p2 with
@@ -921,7 +921,7 @@ let merge_branches t =
 
 
 type prim_aux = 
-  | PAprim of string * constant * CPrimitives.t * prim_aux array
+  | PAprim of string * Constant.t * CPrimitives.t * prim_aux array
   | PAml of mllambda
 
 let add_check cond args =
@@ -1504,7 +1504,7 @@ let string_of_dirpath = function
 (* OCaml as a module identifier.                                           *)
 let string_of_dirpath s = "N"^string_of_dirpath s
 
-let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir)
+let mod_uid_of_dirpath dir = string_of_dirpath (DirPath.repr dir)
 
 let link_info_of_dirpath dir =
   Linked (mod_uid_of_dirpath dir ^ ".")
@@ -1523,19 +1523,19 @@ let string_of_label_def l =
 let rec list_of_mp acc = function
   | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp
   | MPfile dp ->
-      let dp = repr_dirpath dp in
+      let dp = DirPath.repr dp in
       string_of_dirpath dp :: acc
-  | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc
+  | MPbound mbid -> ("X"^string_of_id (MBId.to_id mbid))::acc
 
 let list_of_mp mp = list_of_mp [] mp
 
 let string_of_kn kn =
-  let (mp,dp,l) = repr_kn kn in
+  let (mp,dp,l) = KerName.repr kn in
   let mp = list_of_mp mp in
   String.concat "_" mp ^ "_" ^ string_of_label l
 
-let string_of_con c = string_of_kn (user_con c)
-let string_of_mind mind = string_of_kn (user_mind mind)
+let string_of_con c = string_of_kn (Constant.user c)
+let string_of_mind mind = string_of_kn (MutInd.user mind)
 
 let string_of_gname g =
   match g with
@@ -1877,7 +1877,7 @@ let compile_constant env sigma prefix ~interactive con cb =
         if interactive then LinkedInteractive prefix
         else Linked prefix
       in
-      let l = con_label con in
+      let l = Constant.label con in
       let auxdefs,code =
 	if no_univs then compile_with_fv env sigma None [] (Some l) code
 	else
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index ae6fb1bd6..764598097 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -34,9 +34,9 @@ val get_value : symbols -> int -> Nativevalues.t
 
 val get_sort : symbols -> int -> sorts
 
-val get_name : symbols -> int -> name
+val get_name : symbols -> int -> Name.t
 
-val get_const : symbols -> int -> constant
+val get_const : symbols -> int -> Constant.t
 
 val get_match : symbols -> int -> Nativevalues.annot_sw
 
@@ -60,20 +60,20 @@ val empty_updates : code_location_updates
 
 val register_native_file : string -> unit
 
-val compile_constant_field : env -> string -> constant ->
+val compile_constant_field : env -> string -> Constant.t ->
   global list -> constant_body -> global list
 
-val compile_mind_field : string -> module_path -> label ->
+val compile_mind_field : string -> ModPath.t -> Label.t ->
   global list -> mutual_inductive_body -> global list
 
 val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code
 val mk_norm_code : env -> evars -> string -> constr -> linkable_code
 
-val mk_library_header : dir_path -> global list
+val mk_library_header : DirPath.t -> global list
 
-val mod_uid_of_dirpath : dir_path -> string
+val mod_uid_of_dirpath : DirPath.t -> string
 
-val link_info_of_dirpath : dir_path -> link_info
+val link_info_of_dirpath : DirPath.t -> link_info
 
 val update_locations : code_location_updates -> unit
 
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 73f18f7a7..b2c8662da 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -20,17 +20,17 @@ type uint =
   | UintDecomp of prefix * constructor * lambda
 
 and lambda =
-  | Lrel          of name * int 
+  | Lrel          of Name.t * int 
   | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
   | Levar         of existential * lambda (* type *)
   | Lprod         of lambda * lambda 
-  | Llam          of name array * lambda  
-  | Llet          of name * lambda * lambda
+  | Llam          of Name.t array * lambda  
+  | Llet          of Name.t * lambda * lambda
   | Lapp          of lambda * lambda array
   | Lconst        of prefix * pconstant
-  | Lproj         of prefix * constant (* prefix, projection name *)
-  | Lprim         of prefix * constant * CPrimitives.t * lambda array
+  | Lproj         of prefix * Constant.t (* prefix, projection name *)
+  | Lprim         of prefix * Constant.t * CPrimitives.t * lambda array
   | Lcase         of annot_sw * lambda * lambda * lam_branches 
                   (* annotations, term being matched, accu, branches *)
   | Lif           of lambda * lambda * lambda
@@ -48,6 +48,6 @@ and lambda =
   | Llazy
   | Lforce
 
-and lam_branches = (constructor * name array * lambda) array 
+and lam_branches = (constructor * Name.t array * lambda) array 
 
-and fix_decl =  name array * lambda array * lambda array
+and fix_decl =  Name.t array * lambda array * lambda array
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 508112b35..aaa9f9b00 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -378,7 +378,7 @@ module Renv =
     type constructor_info = tag * int * int (* nparam nrealargs *)
 
     type t = {
-	name_rel : name Vect.t;
+	name_rel : Name.t Vect.t;
 	construct_tbl : constructor_info ConstrTable.t;
 
        }
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 156e4f834..392961f5d 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -18,13 +18,13 @@ type evars =
 
 val empty_evars : evars
 
-val decompose_Llam : lambda -> Names.name array * lambda
-val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda
+val decompose_Llam : lambda -> Name.t array * lambda
+val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda
 
 val is_lazy : prefix -> constr -> bool
 val mk_lazy : lambda -> lambda
 
-val get_mind_prefix : env -> mutual_inductive -> string
+val get_mind_prefix : env -> MutInd.t -> string
 
 val get_alias : env -> pconstant -> pconstant
 
@@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
 val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda ->
 			 lambda
 
-val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array ->
+val compile_prim : CPrimitives.t -> Constant.t -> bool -> prefix -> lambda array ->
 		   lambda
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index a262a9f58..b74d4fdd0 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,7 +21,7 @@ val get_ml_filename : unit -> string * string
 
 val compile : string -> global list -> profile:bool -> bool * string
 
-val compile_library : Names.dir_path -> global list -> string -> bool
+val compile_library : Names.DirPath.t -> global list -> string -> bool
 
 val call_linker :
   ?fatal:bool -> string -> string -> code_location_updates option -> unit
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 3e273dde2..c68f78121 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -26,7 +26,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 = make_con mp empty_dirpath l in
+     let con = Constant.make3 mp DirPath.empty 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/nativelibrary.mli b/kernel/nativelibrary.mli
index f327ba224..72e3d8041 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -13,5 +13,5 @@ open Nativecode
 (** This file implements separate compilation for libraries in the native
 compiler *)
 
-val dump_library : module_path -> dir_path -> env -> module_signature ->
+val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
   global list * symbols
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 1c9996d89..2f8920088 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -58,10 +58,10 @@ type atom =
             (* types, bodies, rec_pos, pos *)
   | Acofix of t array * t array * int * t
   | Acofixe of t array * t array * int * t
-  | Aprod of name * t * (t -> t)
+  | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
   | Aevar of existential * t
-  | Aproj of constant * accumulator
+  | Aproj of Constant.t * accumulator
 
 let accumulate_tag = 0
 
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 0e2db8486..1368b4470 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -49,27 +49,27 @@ type atom =
   | Afix of t array * t array * rec_pos * int 
   | Acofix of t array * t array * int * t
   | Acofixe of t array * t array * int * t
-  | Aprod of name * t * (t -> t)
+  | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
   | Aevar of existential * t
-  | Aproj of constant * accumulator
+  | Aproj of Constant.t * accumulator
 
 (* Constructors *)
 
 val mk_accu : atom -> t
 val mk_rel_accu : int -> t
 val mk_rels_accu : int -> int -> t array
-val mk_constant_accu : constant -> Univ.Level.t array -> t
+val mk_constant_accu : Constant.t -> Univ.Level.t array -> t
 val mk_ind_accu : inductive -> Univ.Level.t array -> t
 val mk_sort_accu : sorts -> Univ.Level.t array -> t
 val mk_var_accu : Id.t -> t
 val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
-val mk_prod_accu : name -> t -> t -> t
+val mk_prod_accu : Name.t -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
 val mk_cofix_accu : int -> t array -> t array -> t
 val mk_meta_accu : metavariable -> t
 val mk_evar_accu : existential -> t -> t
-val mk_proj_accu : constant -> accumulator -> t
+val mk_proj_accu : Constant.t -> accumulator -> t
 val upd_cofix : t -> t -> unit
 val force_cofix : t -> t 
 val mk_const : tag -> t
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f2a009b86..27f9511e1 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -88,9 +88,9 @@ val env_of_named     : Id.t -> env -> env
 (** Global constants *)
 
 
-val lookup_constant_key : constant -> env -> constant_key
-val lookup_constant : constant -> env -> constant_body
+val lookup_constant_key : Constant.t -> env -> constant_key
+val lookup_constant : Constant.t -> env -> constant_body
 
 (** Mutual Inductives *)
-val lookup_mind_key : mutual_inductive -> env -> mind_key
-val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
+val lookup_mind_key : MutInd.t -> env -> mind_key
+val lookup_mind : MutInd.t -> env -> mutual_inductive_body
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2bf9f43a5..79a35d292 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -62,7 +62,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of constant * lift
+  | Zlproj of Constant.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -239,7 +239,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
             | (Zlapp a1,Zlapp a2) -> 
 	       Array.fold_right2 f a1 a2 cu1
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	      if not (eq_constant c1 c2) then 
+	      if not (Constant.equal c1 c2) then 
 		raise NotConvertible
 	      else cu1
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fd024b215..0e416b3e5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -114,7 +114,7 @@ module DPMap = Map.Make(DirPath)
 
 type safe_environment =
   { env : Environ.env;
-    modpath : module_path;
+    modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
     paramresolver : Mod_subst.delta_resolver;
@@ -125,7 +125,7 @@ type safe_environment =
     future_cst : Univ.ContextSet.t Future.computation list;
     engagement : engagement option;
     required : vodigest DPMap.t;
-    loads : (module_path * module_body) list;
+    loads : (ModPath.t * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
     native_symbols : Nativecode.symbols DPMap.t }
 
@@ -143,7 +143,7 @@ let rec library_dp_of_senv senv =
 
 let empty_environment =
   { env = Environ.empty_env;
-    modpath = initial_path;
+    modpath = ModPath.initial;
     modvariant = NONE;
     modresolver = Mod_subst.empty_delta_resolver;
     paramresolver = Mod_subst.empty_delta_resolver;
@@ -160,7 +160,7 @@ let empty_environment =
 
 let is_initial senv =
   match senv.revstruct, senv.modvariant with
-  | [], NONE -> ModPath.equal senv.modpath initial_path
+  | [], NONE -> ModPath.equal senv.modpath ModPath.initial
   | _ -> false
 
 let delta_of_senv senv = senv.modresolver,senv.paramresolver
@@ -458,8 +458,8 @@ let constraints_of_sfb env sfb =
     It also performs the corresponding [add_constraints]. *)
 
 type generic_name =
-  | C of constant
-  | I of mutual_inductive
+  | C of Constant.t
+  | I of MutInd.t
   | M (** name already known, cf the mod_mp field *)
   | MT (** name already known, cf the mod_mp field *)
 
@@ -502,7 +502,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constant_role
+  Constant.t * private_constant_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
@@ -521,7 +521,7 @@ let add_constant_aux no_section senv (kn, cb) =
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
       update_resolver
-        (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv'
+        (Mod_subst.add_inline_delta_resolver (Constant.user kn) (lev,None)) senv'
     | _ -> senv'
   in
   senv''
@@ -535,7 +535,7 @@ let export_private_constants ~in_section ce senv =
   (ce, exported), senv
 
 let add_constant dir l decl senv =
-  let kn = make_con senv.modpath dir l in
+  let kn = Constant.make3 senv.modpath dir l in
   let no_section = DirPath.is_empty dir in
   let senv =
     let cb = 
@@ -562,7 +562,7 @@ let check_mind mie lab =
 
 let add_mind dir l mie senv =
   let () = check_mind mie l in
-  let kn = make_mind senv.modpath dir l in
+  let kn = MutInd.make3 senv.modpath dir 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
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f0f273f35..ee9632944 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -60,8 +60,8 @@ val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
 
-val private_con_of_con : safe_environment -> constant -> private_constant
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
+val private_con_of_con : safe_environment -> Constant.t -> private_constant
+val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant
 
 val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
@@ -103,7 +103,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constant_role
+  Constant.t * private_constant_role
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.constant_entry ->
@@ -113,22 +113,22 @@ val export_private_constants : in_section:bool ->
     unless one requires the side effects to be exported) *)
 val add_constant :
   DirPath.t -> Label.t -> global_declaration ->
-    constant safe_transformer
+    Constant.t safe_transformer
 
 (** Adding an inductive type *)
 
 val add_mind :
   DirPath.t -> Label.t -> Entries.mutual_inductive_entry ->
-    mutual_inductive safe_transformer
+    MutInd.t safe_transformer
 
 (** Adding a module or a module type *)
 
 val add_module :
   Label.t -> Entries.module_entry -> Declarations.inline ->
-    (module_path * Mod_subst.delta_resolver) safe_transformer
+    (ModPath.t * Mod_subst.delta_resolver) safe_transformer
 val add_modtype :
   Label.t -> Entries.module_type_entry -> Declarations.inline ->
-    module_path safe_transformer
+    ModPath.t safe_transformer
 
 (** Adding universe constraints *)
 
@@ -150,9 +150,9 @@ val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 
 (** {6 Interactive module functions } *)
 
-val start_module : Label.t -> module_path safe_transformer
+val start_module : Label.t -> ModPath.t safe_transformer
 
-val start_modtype : Label.t -> module_path safe_transformer
+val start_modtype : Label.t -> ModPath.t safe_transformer
 
 val add_module_parameter :
   MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
@@ -166,17 +166,17 @@ val allow_delayed_constants : bool ref
 
 val end_module :
   Label.t -> (Entries.module_struct_entry * Declarations.inline) option ->
-    (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer
+    (ModPath.t * MBId.t list * Mod_subst.delta_resolver) safe_transformer
 
-val end_modtype : Label.t -> (module_path * MBId.t list) safe_transformer
+val end_modtype : Label.t -> (ModPath.t * MBId.t list) safe_transformer
 
 val add_include :
   Entries.module_struct_entry -> bool -> Declarations.inline ->
    Mod_subst.delta_resolver safe_transformer
 
-val current_modpath : safe_environment -> module_path
+val current_modpath : safe_environment -> ModPath.t
 
-val current_dirpath : safe_environment -> dir_path
+val current_dirpath : safe_environment -> DirPath.t
 
 (** {6 Libraries : loading and saving compilation units } *)
 
@@ -186,16 +186,16 @@ type native_library = Nativecode.global list
 
 val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
 
-val start_library : DirPath.t -> module_path safe_transformer
+val start_library : DirPath.t -> ModPath.t safe_transformer
 
 val export :
   ?except:Future.UUIDSet.t ->
   safe_environment -> DirPath.t ->
-    module_path * compiled_library * native_library
+    ModPath.t * compiled_library * native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
 val import : compiled_library -> Univ.universe_context_set -> vodigest ->
-  module_path safe_transformer
+  ModPath.t safe_transformer
 
 (** {6 Safe typing judgments } *)
 
@@ -223,7 +223,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 val register :
   field -> Retroknowledge.entry -> Term.constr -> safe_transformer0
 
-val register_inline : constant -> safe_transformer0
+val register_inline : Constant.t -> safe_transformer0
 
 val set_strategy :
-  safe_environment -> Names.constant Names.tableKey -> Conv_oracle.level -> safe_environment
+  safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index b564b2a8c..d8e281d52 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -63,11 +63,11 @@ let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty }
 
 let get_obj mp map l =
   try Label.Map.find l map.objs
-  with Not_found -> error_no_such_label_sub l (string_of_mp mp)
+  with Not_found -> error_no_such_label_sub l (ModPath.to_string mp)
 
 let get_mod mp map l =
   try Label.Map.find l map.mods
-  with Not_found -> error_no_such_label_sub l (string_of_mp mp)
+  with Not_found -> error_no_such_label_sub l (ModPath.to_string mp)
 
 let make_labmap mp list =
   let add_one (l,e) map =
@@ -181,7 +181,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
 	cst
   in
-  let mind = mind_of_kn kn1 in
+  let mind = MutInd.make1 kn1 in
   let check_cons_types i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
diff --git a/kernel/term.ml b/kernel/term.ml
index 0e0af2f59..161abfba1 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -67,7 +67,7 @@ type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
 type 'a puniverses = 'a Univ.puniverses
 
 (** Simply type aliases *)
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -83,7 +83,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of (constant * 'univs)
+  | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
diff --git a/kernel/term.mli b/kernel/term.mli
index d5aaf6ad0..051979180 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -26,7 +26,7 @@ type sorts_family = Sorts.family = InProp | InSet | InType
 type 'a puniverses = 'a Univ.puniverses
 
 (** Simply type aliases *)
-type pconstant = constant puniverses
+type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
@@ -80,7 +80,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Lambda    of Name.t * 'types * 'constr
   | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of (constant * 'univs)
+  | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
   | Case      of case_info * 'constr * 'constr * 'constr array
@@ -165,7 +165,7 @@ val decompose_app : constr -> constr * constr list
 val decompose_appvect : constr -> constr * constr array
 
 (** Destructs a constant *)
-val destConst : constr -> constant puniverses
+val destConst : constr -> Constant.t puniverses
 
 (** Destructs an existential variable *)
 val destEvar : constr -> existential
@@ -415,11 +415,11 @@ val mkProd : Name.t * types * types -> types
 val mkLambda : Name.t * types * constr -> constr
 val mkLetIn : Name.t * constr * types * constr -> constr
 val mkApp : constr * constr array -> constr
-val mkConst : constant -> constr
+val mkConst : Constant.t -> constr
 val mkProj : projection * constr -> constr
 val mkInd : inductive -> constr
 val mkConstruct : constructor -> constr
-val mkConstU : constant puniverses -> constr
+val mkConstU : Constant.t puniverses -> constr
 val mkIndU : inductive puniverses -> constr
 val mkConstructU : constructor puniverses -> constr
 val mkConstructUi : (pinductive * int) -> constr
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index e28c8e826..d50abf071 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -525,7 +525,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effect_role
+  Constant.t * constant_body * side_effect_role
 
 let export_side_effects mb env ce =
   match ce with
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b16f81c5a..815269169 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -47,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-  'a trust -> env -> constant -> 'a constant_entry ->
+  'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
 type side_effect_role =
@@ -55,7 +55,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effect_role
+  Constant.t * constant_body * side_effect_role
   
 (* Given a constant entry containing side effects it exports them (either
  * by re-checking them or trusting them).  Returns the constant bodies to
@@ -66,14 +66,14 @@ val export_side_effects :
     exported_side_effect list * unit constant_entry
 
 val translate_mind :
-  env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
+  env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
-val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
+val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:'a trust -> env -> constant option -> 
+val infer_declaration : trust:'a trust -> env -> Constant.t option -> 
   'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  constant -> env -> Cooking.result -> constant_body
+  Constant.t -> env -> Cooking.result -> constant_body
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b40badd7c..f99f34b06 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -298,7 +298,7 @@ let type_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
-  assert(eq_mind pb.proj_ind (fst ind));
+  assert(MutInd.equal pb.proj_ind (fst ind));
   let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
   substl (c :: List.rev args) ty
       
diff --git a/kernel/vars.ml b/kernel/vars.ml
index d0dad02ec..f52d734ef 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -354,5 +354,5 @@ let subst_instance_context s ctx =
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
 
-type id_key = constant tableKey
+type id_key = Constant.t tableKey
 let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 59dc09a75..ae846fd42 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -144,5 +144,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co
 val subst_instance_constr : universe_instance -> constr -> constr
 val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t
 
-type id_key = constant tableKey
+type id_key = Constant.t tableKey
 val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 6b7a86d6f..4e13881b8 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -357,7 +357,7 @@ let val_of_proj kn v =
 
 module IdKeyHash =
 struct
-  type t = constant tableKey
+  type t = Constant.t tableKey
   let equal = Names.eq_table_key Constant.equal
   open Hashset.Combine
   let hash = function
@@ -654,10 +654,10 @@ let apply_whd k whd =
 let rec pr_atom a =
   Pp.(match a with
   | Aid c -> str "Aid(" ++ (match c with
-                            | ConstKey c -> Names.pr_con c
+                            | ConstKey c -> Constant.print c
 			    | RelKey i -> str "#" ++ int i
 			    | _ -> str "...") ++ str ")"
-  | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")"
+  | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")"
   | Atype _ -> str "Atype(")
 and pr_whd w =
   Pp.(match w with
@@ -679,4 +679,4 @@ and pr_zipper z =
   | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
   | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
   | Zswitch s -> str "Zswitch(...)"
-  | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")")
+  | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")")
diff --git a/kernel/vm.mli b/kernel/vm.mli
index df638acc1..ea38ee43f 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -59,7 +59,7 @@ val pr_stack : stack -> Pp.t
 val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
 val val_of_named : Id.t -> values
-val val_of_constant : constant -> values
+val val_of_constant : Constant.t -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 1e3c37a9e..17c79d2e1 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 *)
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index cbf5788e4..327ee0015 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -124,7 +124,7 @@ val prepare_predicate : ?loc:Loc.t ->
            (types * tomatch_type) list ->
            (rel_context * rel_context) list ->
            constr option ->
-           glob_constr option -> (Evd.evar_map * Names.name list * constr) list
+           glob_constr option -> (Evd.evar_map * Name.t list * constr) list
 
-val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t ->
   Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 260cd0444..fe969f9e5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -27,9 +27,9 @@ type cl_typ =
   | CL_SORT
   | CL_FUN
   | CL_SECVAR of variable
-  | CL_CONST of constant
+  | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of constant
+  | CL_PROJ of Constant.t
 
 type cl_info_typ = {
   cl_param : int
@@ -59,8 +59,8 @@ let coe_info_typ_equal c1 c2 =
 
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2
   | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8707078b5..b41d0efac 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -17,9 +17,9 @@ type cl_typ =
   | CL_SORT
   | CL_FUN
   | CL_SECVAR of variable
-  | CL_CONST of constant
+  | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of constant
+  | CL_PROJ of Constant.t
 
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ddef1cee9..b7b76c830 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -214,7 +214,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
   let convref ref c = 
     match ref, EConstr.kind sigma c with
     | VarRef id, Var id' -> Names.Id.equal id id'
-    | ConstRef c, Const (c',_) -> Names.eq_constant c c'
+    | ConstRef c, Const (c',_) -> Constant.equal c c'
     | IndRef i, Ind (i', _) -> Names.eq_ind i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
     | _, _ -> 
@@ -286,7 +286,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
 	(match c1, EConstr.kind sigma c2 with
-	| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr))
+	| PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
 	    || Projection.unfolded pr ->
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
@@ -303,7 +303,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
       | PApp (PRef (ConstRef c1), _), Proj (pr, c2) 
-	when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> 
+	when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> 
 	raise PatternMatchingFailure
 	
       | PApp (c, args), Proj (pr, c2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0f1a508c8..45fe2b2d8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -297,7 +297,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
     | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
-       if eq_constant (Projection.constant p1) (Projection.constant p2)
+       if Constant.equal (Projection.constant p1) (Projection.constant p2)
        then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
@@ -341,7 +341,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 	  (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
     | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
-       if eq_constant (Projection.constant p1) (Projection.constant p2)
+       if Constant.equal (Projection.constant p1) (Projection.constant p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
@@ -771,7 +771,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    ise_try evd [f1; f2]
 	      
 	(* Catch the p.c ~= p c' cases *)
-	| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
+	| Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' ->
 	  let res = 
 	    try Some (destApp evd (Retyping.expand_projection env evd p c []))
 	    with Retyping.RetypeError _ -> None
@@ -782,7 +782,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		(appr2,csts2)
 	    | None -> UnifFailure (evd,NotSameHead))
 	      
-	| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
+	| Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
 	  let res = 
 	    try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
 	    with Retyping.RetypeError _ -> None
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index f27928662..9dd7068cb 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -64,7 +64,7 @@ val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_
     here by its relevant components [m] and [c]. It is used to
     interpret Ltac-bound names both in pretyping and printing of
     terms. *)
-val map_pattern_binders : (name -> name) ->
+val map_pattern_binders : (Name.t -> Name.t) ->
   tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
 
 (** [map_pattern f m c] applies [f] to the return predicate and the
@@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob
 
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
-val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name
+val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
 val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index aced42f83..0cb5974e8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -566,7 +566,7 @@ let build_mutual_induction_scheme env sigma = function
     	(List.map
 	   (function ((mind',u'),dep',s') ->
 	      let (sp',_) = mind' in
-	      if eq_mind sp sp' then
+	      if MutInd.equal sp sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		((mind',u'),mibi',mipi',dep',s')
 	      else
@@ -605,7 +605,7 @@ let lookup_eliminator ind_sp s =
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in
+    let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in
     let _ = Global.lookup_constant cst in
       ConstRef cst
   with Not_found ->
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index aa38d3b47..65d5161df 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -147,7 +147,7 @@ val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
 val get_constructors : env -> inductive_family -> constructor_summary array
-val get_projections  : env -> inductive_family -> constant array option
+val get_projections  : env -> inductive_family -> Constant.t array option
 
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index aaa946706..fd76a9473 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -174,7 +174,7 @@ let pattern_of_constr env sigma t =
          with
          | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
          | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
-    | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
+    | Const (sp,u)  -> PRef (ConstRef (Constant.make1 (Constant.canonical sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e970a1db9..4f4e49d82 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -37,7 +37,7 @@ type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
   s_PROJKIND : (Name.t * bool) list;
-  s_PROJ : constant option list }
+  s_PROJ : Constant.t option list }
 
 let structure_table =
   Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
@@ -48,7 +48,7 @@ let projection_table =
    is the inductive always (fst constructor) ? It seems so... *)
 
 type struc_tuple =
-    inductive * constructor * (Name.t * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * Constant.t option list
 
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -286,7 +286,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
 let discharge_canonical_structure (_,(cst,ind)) =
   Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
 
-let inCanonStruc : constant * inductive -> obj =
+let inCanonStruc : Constant.t * inductive -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 8e2333b34..066623164 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -20,10 +20,10 @@ type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
   s_PROJKIND : (Name.t * bool) list;
-  s_PROJ : constant option list }
+  s_PROJ : Constant.t option list }
 
 type struc_tuple =
-    inductive * constructor * (Name.t * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * Constant.t option list
 
 val declare_structure : struc_tuple -> unit
 
@@ -35,7 +35,7 @@ val lookup_structure : inductive -> struc_typ
 (** [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
    it fails with [Not_found] *)
-val lookup_projections : inductive -> constant option list
+val lookup_projections : inductive -> Constant.t option list
 
 (** raise [Not_found] if not a projection *)
 val find_projection_nparams : global_reference -> int
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2aa2f9013..308896f3a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -358,7 +358,7 @@ struct
        ++ str ")"
     | Proj (n,m,p,cst) ->
       str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
-	pr_comma () ++ pr_con (Projection.constant p) ++ str ")"
+	pr_comma () ++ Constant.print (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Termops.pr_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1828196fe..950fcdee4 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -258,7 +258,7 @@ val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixp
 val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
-val is_transparent : Environ.env -> constant tableKey -> bool
+val is_transparent : Environ.env -> Constant.t tableKey -> bool
 
 (** {6 Conversion Functions (uses closures, lazy strategy) } *)
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9451b0f86..85383ba39 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -75,13 +75,13 @@ let global_of_evaluable_reference = function
   | EvalVarRef id -> VarRef id
 
 type evaluable_reference =
-  | EvalConst of constant
+  | EvalConst of Constant.t
   | EvalVar of Id.t
   | EvalRel of int
   | EvalEvar of EConstr.existential
 
 let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
-| EvalConst c1, EvalConst c2 -> eq_constant c1 c2
+| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
@@ -240,7 +240,7 @@ let invert_name labs l na0 env sigma ref = function
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
 	  | EvalConst kn ->
-	      Some (EvalConst (con_with_label kn (Label.of_id id))) in
+	      Some (EvalConst (Constant.change_label kn (Label.of_id id))) in
 	match refi with
 	  | None -> None
 	  | Some ref ->
@@ -521,7 +521,7 @@ let reduce_mind_case_use_function func env sigma mia =
 		       the block was indeed initially built as a global
 		       definition *)
                     let (kn, u) = destConst sigma func in
-                    let kn = con_with_label kn (Label.of_id id) in
+                    let kn = Constant.change_label kn (Label.of_id id) in
                     let cst = (kn, EInstance.kind sigma u) in
 		    try match constant_opt_value_in env cst with
 		      | None -> None
@@ -944,7 +944,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       | CoFix _ | Fix _ -> s'
       | Proj (p,t) when
 	  (match EConstr.kind sigma constr with
-	  | Const (c', _) -> eq_constant (Projection.constant p) c'
+	  | Const (c', _) -> Constant.equal (Projection.constant p) c'
 	  | _ -> false) ->
 	let pb = Environ.lookup_projection p env in
 	  if List.length stack <= pb.Declarations.proj_npars then
@@ -1050,7 +1050,7 @@ let contextually byhead occs f env sigma t =
 
 let match_constr_evaluable_ref sigma c evref = 
   match EConstr.kind sigma c, evref with
-  | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
+  | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u
   | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 375a8a983..1e06e9f8c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -71,7 +71,7 @@ type typeclass = {
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
-	      * constant option) list;
+	      * Constant.t option) list;
   
   cl_strict : bool;
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 99cdbd3a3..20fbbb5a0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -36,7 +36,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8f7e2bba..01c28b5ed 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -554,10 +554,10 @@ let oracle_order env cf1 cf2 =
       | Some k2 ->
 	match k1, k2 with
 	| IsProj (p, _), IsKey (ConstKey (p',_)) 
-	  when eq_constant (Projection.constant p) p' -> 
+	  when Constant.equal (Projection.constant p) p' -> 
 	  Some (not (Projection.unfolded p))
 	| IsKey (ConstKey (p,_)), IsProj (p', _) 
-	  when eq_constant p (Projection.constant p') -> 
+	  when Constant.equal p (Projection.constant p') -> 
 	  Some (Projection.unfolded p')
 	| _ ->
           Some (Conv_oracle.oracle_order (fun x -> x)
@@ -784,7 +784,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
 
 	(** Fast path for projections. *)
-	| Proj (p1,c1), Proj (p2,c2) when eq_constant
+	| Proj (p1,c1), Proj (p2,c2) when Constant.equal
 	    (Projection.constant p1) (Projection.constant p2) ->
 	  (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
 	       substn c1 c2
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fdaeded87..f69c4bce7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -33,12 +33,12 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : mutual_inductive -> Pp.t;
-  print_constant_with_infos : constant -> Pp.t;
+  print_inductive           : MutInd.t -> Pp.t;
+  print_constant_with_infos : Constant.t -> Pp.t;
   print_section_variable    : variable -> Pp.t;
-  print_syntactic_def       : kernel_name -> Pp.t;
-  print_module              : bool -> Names.module_path -> Pp.t;
-  print_modtype             : module_path -> Pp.t;
+  print_syntactic_def       : KerName.t -> Pp.t;
+  print_module              : bool -> ModPath.t -> Pp.t;
+  print_modtype             : ModPath.t -> Pp.t;
   print_named_decl          : Context.Named.Declaration.t -> Pp.t;
   print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
   print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
@@ -318,8 +318,8 @@ type locatable = Locatable : 'a locatable_info -> locatable
 type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
-  | Syntactic of kernel_name
-  | ModuleType of module_path
+  | Syntactic of KerName.t
+  | ModuleType of ModPath.t
   | Other : 'a * 'a locatable_info -> logical_name
   | Undefined of qualid
 
@@ -623,14 +623,14 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
              constraints *)
 	  (try Some(print_named_decl (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
-	  Some (print_constant with_values sep (constant_of_kn kn))
+	  Some (print_constant with_values sep (Constant.make1 kn))
       | (_,"INDUCTIVE") ->
-	  Some (gallina_print_inductive (mind_of_kn kn))
+	  Some (gallina_print_inductive (MutInd.make1 kn))
       | (_,"MODULE") ->
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	    Some (print_module with_values (MPdot (mp,l)))
       | (_,"MODULE TYPE") ->
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	  Some (print_modtype (MPdot (mp,l)))
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
 	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
@@ -750,12 +750,12 @@ let print_full_pure_context () =
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | "MODULE TYPE" ->
 	  (* TODO: make it reparsable *)
 	  (* TODO: make it reparsable *)
-	  let (mp,_,l) = repr_kn kn in
+	  let (mp,_,l) = KerName.repr kn in
 	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | _ -> mt () in
       prec rest ++ pp
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index dbd101159..31fd766ea 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -80,12 +80,12 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : mutual_inductive -> Pp.t;
-  print_constant_with_infos : constant -> Pp.t;
+  print_inductive           : MutInd.t -> Pp.t;
+  print_constant_with_infos : Constant.t -> Pp.t;
   print_section_variable    : variable -> Pp.t;
-  print_syntactic_def       : kernel_name -> Pp.t;
-  print_module              : bool -> Names.module_path -> Pp.t;
-  print_modtype             : module_path -> Pp.t;
+  print_syntactic_def       : KerName.t -> Pp.t;
+  print_module              : bool -> ModPath.t -> Pp.t;
+  print_modtype             : ModPath.t -> Pp.t;
   print_named_decl          : Context.Named.Declaration.t -> Pp.t;
   print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
   print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 70e96722d..e4bb89304 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -855,15 +855,15 @@ let prterm = pr_lconstr
    It is used primarily by the Print Assumptions command. *)
 
 type axiom =
-  | Constant of constant (* An axiom or a constant. *)
+  | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
-  | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of axiom * (Label.t * Context.Rel.t * types) list
-  | Opaque of constant     (* An opaque constant. *)
-  | Transparent of constant
+  | Opaque of Constant.t     (* An opaque constant. *)
+  | Transparent of Constant.t
 
 (* Defines a set of [assumption] *)
 module OrderedContextObject =
@@ -873,11 +873,11 @@ struct
   let compare_axiom x y =
     match x,y with
     | Constant k1 , Constant k2 ->
-        con_ord k1 k2
+        Constant.CanOrd.compare k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
-        con_ord k1 k2
+        Constant.CanOrd.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
     | _ -> -1
@@ -890,10 +890,10 @@ struct
     | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2
     | Axiom _ , _ -> -1
     | _ , Axiom _ -> 1
-    | Opaque k1 , Opaque k2 -> con_ord k1 k2
+    | Opaque k1 , Opaque k2 -> Constant.CanOrd.compare k1 k2
     | Opaque _ , _ -> -1
     | _ , Opaque _ -> 1
-    | Transparent k1 , Transparent k2 -> con_ord k1 k2
+    | Transparent k1 , Transparent k2 -> Constant.CanOrd.compare k1 k2
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
@@ -907,8 +907,8 @@ let pr_assumptionset env s =
     let safe_pr_constant env kn =
       try pr_constant env kn
       with Not_found ->
-	let mp,_,lab = repr_con kn in
-        str (string_of_mp mp) ++ str "." ++ pr_label lab
+	let mp,_,lab = Constant.repr3 kn in
+        str (ModPath.to_string mp) ++ str "." ++ Label.print lab
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ
@@ -942,7 +942,7 @@ let pr_assumptionset env s =
         let ax = pr_axiom env axiom typ ++
           cut() ++
           prlist_with_sep cut (fun (lbl, ctx, ty) ->
-            str " used in " ++ pr_label lbl ++
+            str " used in " ++ Label.print lbl ++
             str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
           l in
         (v, ax :: a, o, tr)
diff --git a/printing/printer.mli b/printing/printer.mli
index f55206f0d..e74f47efe 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -110,7 +110,7 @@ val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> Pp.t
 val pr_global_env          : Id.Set.t -> global_reference -> Pp.t
 val pr_global              : global_reference -> Pp.t
 
-val pr_constant            : env -> constant -> Pp.t
+val pr_constant            : env -> Constant.t -> Pp.t
 val pr_existential_key     : evar_map -> existential_key -> Pp.t
 val pr_existential         : env -> evar_map -> existential -> Pp.t
 val pr_constructor         : env -> constructor -> Pp.t
@@ -183,15 +183,15 @@ val prterm                 : constr -> Pp.t (** = pr_lconstr *)
 
 (** Declarations for the "Print Assumption" command *)
 type axiom =
-  | Constant of constant (* An axiom or a constant. *)
+  | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
-  | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of axiom * (Label.t * Context.Rel.t * types) list
-  | Opaque of constant     (* An opaque constant. *)
-  | Transparent of constant
+  | Opaque of Constant.t     (* An opaque constant. *)
+  | Transparent of Constant.t
 
 module ContextObjectSet : Set.S with type elt = context_object
 module ContextObjectMap : CMap.ExtS
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 755e905a7..d4b756346 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -301,7 +301,7 @@ let nametab_register_modparam mbid mtb =
       id
 
 let print_body is_impl env mp (l,body) =
-  let name = pr_label l in
+  let name = Label.print l in
   hov 2 (match body with
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 8c3f0149e..b0bbb21e0 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,6 @@ open Names
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> Pp.t
-val print_module : bool -> module_path -> Pp.t
-val print_modtype : module_path -> Pp.t
+val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val print_module : bool -> ModPath.t -> Pp.t
+val print_modtype : ModPath.t -> Pp.t
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c03a3ba6..881000219 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -374,16 +374,16 @@ let find_elim hdcncl lft2rgt dep cls ot =
         | Some true, None
         | Some false, Some _ ->
 	  let c1 = destConstRef pr1 in 
-	  let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in 
+	  let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in 
 	  let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in 
-	  let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in
+	  let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in
 	  begin 
 	    try 
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
 	      user_err ~hdr:"Equality.find_elim"
-                (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
+                (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
         end
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 7f087ea01..240b5a7e0 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -29,7 +29,7 @@ open Pp
 (* Registering schemes in the environment *)
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
   internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
@@ -57,7 +57,7 @@ let discharge_scheme (_,(kind,l)) =
   Some (kind,Array.map (fun (ind,const) ->
     (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
 
-let inScheme : string * (inductive * constant) array -> obj =
+let inScheme : string * (inductive * Constant.t) array -> obj =
   declare_object {(default_object "SCHEME") with
                     cache_function = cache_scheme;
                     load_function = (fun _ -> cache_scheme);
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index f825c4f4a..232a193ac 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -20,7 +20,7 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
   internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
@@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind -> 
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> constant * Safe_typing.private_constants
+  Id.t option -> inductive -> Constant.t * Safe_typing.private_constants
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
+  (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07eea7b63..fe733899f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -622,7 +622,7 @@ module New = struct
       | _ ->
 	  let name_elim =
 	    match EConstr.kind sigma elim with
-	    | Const (kn, _) -> string_of_con kn
+	    | Const (kn, _) -> Constant.to_string kn
 	    | Var id -> Id.to_string id
 	    | _ -> "\b"
 	  in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f67606d2..866daa904 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -580,7 +580,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   | (f, n, ar) :: oth ->
     let open Context.Named.Declaration in
     let (sp', u')  = check_mutind env sigma n ar in
-    if not (eq_mind sp sp') then
+    if not (MutInd.equal sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
@@ -1607,7 +1607,7 @@ let general_elim_clause with_evars flags id c e =
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
 type conjunction_status =
-  | DefinedRecord of constant option list
+  | DefinedRecord of Constant.t option list
   | NotADefinedRecordUseScheme of constr
 
 let make_projection env sigma params cstr sign elim i n c u =
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 6711b14da..09e645eea 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -89,7 +89,7 @@ and fields_of_mp mp =
   let mb = lookup_module_in_impl mp in
   let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
   let subs =
-    if mp_eq inner_mp mp then subs
+    if ModPath.equal inner_mp mp then subs
     else add_mp inner_mp mp mb.mod_delta subs
   in
   Modops.subst_structure subs fields
@@ -118,7 +118,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x
 
 let lookup_constant_in_impl cst fallback =
   try
-    let mp,dp,lab = repr_kn (canonical_con cst) in
+    let mp,dp,lab = KerName.repr (Constant.canonical cst) in
     let fields = memoize_fields_of_mp mp in
     (* A module found this way is necessarily closed, in particular
        our constant cannot be in an opened section : *)
@@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback =
        - The label has not been found in the structure. This is an error *)
     match fallback with
       | Some cb -> cb
-      | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".")
+      | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".")
 
 let lookup_constant cst =
   try
@@ -142,7 +142,7 @@ let lookup_constant cst =
 
 let lookup_mind_in_impl mind =
   try
-    let mp,dp,lab = repr_kn (canonical_mind mind) in
+    let mp,dp,lab = KerName.repr (MutInd.canonical mind) in
     let fields = memoize_fields_of_mp mp in
       search_mind_label lab fields
   with Not_found ->
@@ -156,9 +156,9 @@ let lookup_mind mind =
     traversed objects *)
 
 let label_of = function
-  | ConstRef kn -> pi3 (repr_con kn)
+  | ConstRef kn -> pi3 (Constant.repr3 kn)
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
+  | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn)
   | VarRef id -> Label.of_id id
 
 let fold_constr_with_full_binders g f n acc c =
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 46730f824..77eb968d4 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -21,7 +21,7 @@ open Printer
 val traverse :
   Label.t -> constr ->
     (Refset_env.t * Refset_env.t Refmap_env.t *
-     (label * Context.Rel.t * types) list Refmap_env.t)
+     (Label.t * Context.Rel.t * types) list Refmap_env.t)
 
 (** Collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type). The above warning of
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 66a4a2e49..539e5550f 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -199,7 +199,7 @@ let build_beq_scheme mode kn =
         | Cast (x,_,_) -> aux (EConstr.applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> 
-            if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
+            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
             else begin
               try
                 let eq, eff =
@@ -367,8 +367,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
       (* if this happen then the args have to be already declared as a
               Parameter*)
       (
-        let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
-          mkConst (make_con mp dir (mk_label (
+        let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+          mkConst (Constant.make3 mp dir (Label.make (
           if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
                        else ((Label.to_string lbl)^"_lb")
         )))
@@ -428,8 +428,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
       (* if this happen then the args have to be already declared as a
          Parameter*)
       (
-        let mp,dir,lbl = repr_con (fst (destConst sigma v)) in
-          mkConst (make_con mp dir (mk_label (
+        let mp,dir,lbl = Constant.repr3 (fst (destConst sigma v)) in
+          mkConst (Constant.make3 mp dir (Label.make (
           if Int.equal offset 1 then ("eq_"^(Label.to_string lbl))
                        else ((Label.to_string lbl)^"_bl")
         )))
@@ -504,7 +504,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp2,i2) ->
-  if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
+  if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
   then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
@@ -531,7 +531,7 @@ let eqI ind l =
   and e, eff = 
     try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff 
     with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
-      (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
+      (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
   in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff
 
 (**********************************************************************)
diff --git a/vernac/class.ml b/vernac/class.ml
index 3915148a0..061f3efcc 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -173,8 +173,8 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp)
-  | CL_IND (sp,_) -> Label.to_string (mind_label sp)
+  | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+  | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
   | CL_SECVAR id -> Id.to_string id
 
 (* Identity coercion *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0926c93e5..9a8fc9bc2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -98,7 +98,7 @@ let type_ctx_instance evars env ctx inst subst =
 
 let id_of_class cl =
   match cl.cl_impl with
-    | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l
+    | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l
     | IndRef (kn,i) ->
 	let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
 	  mip.(0).Declarations.mind_typename
diff --git a/vernac/command.mli b/vernac/command.mli
index afa97aa24..26b1d1aaf 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -90,7 +90,7 @@ val interp_mutual_inductive :
 
 val declare_mutual_inductive_with_eliminations :
   mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
-  mutual_inductive
+  MutInd.t
 
 (** Entry points for the vernacular commands Inductive and CoInductive *)
 
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 189c47aab..7b1a948ed 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -899,11 +899,11 @@ let explain_not_match_error = function
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
-  str "Signature components for label " ++ pr_label l ++
+  str "Signature components for label " ++ Label.print l ++
   str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
 
 let explain_label_already_declared l =
-  str "The label " ++ pr_label l ++ str " is already declared."
+  str "The label " ++ Label.print l ++ str " is already declared."
 
 let explain_application_to_not_path _ =
   strbrk "A module cannot be applied to another module application or " ++
@@ -933,11 +933,11 @@ let explain_not_equal_module_paths mp1 mp2 =
   str "Non equal modules."
 
 let explain_no_such_label l =
-  str "No such label " ++ pr_label l ++ str "."
+  str "No such label " ++ Label.print l ++ str "."
 
 let explain_incompatible_labels l l' =
   str "Opening and closing labels are not the same: " ++
-  pr_label l ++ str " <> " ++ pr_label l' ++ str "!"
+  Label.print l ++ str " <> " ++ Label.print l' ++ str "!"
 
 let explain_not_a_module s =
   quote (str s) ++ str " is not a module."
@@ -946,19 +946,19 @@ let explain_not_a_module_type s =
   quote (str s) ++ str " is not a module type."
 
 let explain_not_a_constant l =
-  quote (pr_label l) ++ str " is not a constant."
+  quote (Label.print l) ++ str " is not a constant."
 
 let explain_incorrect_label_constraint l =
   str "Incorrect constraint for label " ++
-  quote (pr_label l) ++ str "."
+  quote (Label.print l) ++ str "."
 
 let explain_generative_module_expected l =
-  str "The module " ++ pr_label l ++ str " is not generative." ++
+  str "The module " ++ Label.print l ++ str " is not generative." ++
   strbrk " Only components of generative modules can be changed" ++
   strbrk " using the \"with\" construct."
 
 let explain_label_missing l s =
-  str "The field " ++ pr_label l ++ str " is missing in "
+  str "The field " ++ Label.print l ++ str " is missing in "
   ++ str s ++ str "."
 
 let explain_include_restricted_functor mp =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 90168843a..4bdc93a36 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -407,7 +407,7 @@ let do_mutual_induction_scheme lnamedepindsort =
 let get_common_underlying_mutual_inductive = function
   | [] -> assert false
   | (id,(mind,i as ind))::l as all ->
-      match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with
+      match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
       | (_,ind')::_ ->
 	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
       | [] ->
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 91c4c5825..659f12936 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -16,9 +16,9 @@ open Vernacexpr
 
 (** Build and register the boolean equalities associated to an inductive type *)
 
-val declare_beq_scheme : mutual_inductive -> unit
+val declare_beq_scheme : MutInd.t -> unit
 
-val declare_eq_decidability : mutual_inductive -> unit
+val declare_eq_decidability : MutInd.t -> unit
 
 (** Build and register a congruence scheme for an equality-like inductive type *)
 
@@ -39,10 +39,10 @@ val do_scheme : (Id.t located option * scheme) list -> unit
 
 (** Combine a list of schemes into a conjunction of them *)
 
-val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types
+val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
 
 val do_combined_scheme : Id.t located -> Id.t located list -> unit
 
 (** Hook called at each inductive type definition *)
 
-val declare_default_schemes : mutual_inductive -> unit
+val declare_default_schemes : MutInd.t -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index dbf7fec66..22f0d199c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -116,7 +116,7 @@ let find_mutually_recursive_statements thms =
             [] in
       ind_hyps,ind_ccl) thms in
     let inds_hyps,ind_ccls = List.split inds in
-    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> MutInd.equal kn kn' in
     (* Check if all conclusions are coinductive in the same type *)
     (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =
diff --git a/vernac/record.mli b/vernac/record.mli
index aea474581..1bcbf39b7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ val primitive_flag : bool ref
 val declare_projections :
   inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
   coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
-  (Name.t * bool) list * constant option list
+  (Name.t * bool) list * Constant.t option list
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 41f63644d..7eedf24f8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -250,7 +250,7 @@ let print_namespace ns =
   let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
   let print_kn kn =
     (* spiwack: I'm ignoring the dirpath, is that bad? *)
-    let (mp,_,lbl) = Names.repr_kn kn in
+    let (mp,_,lbl) = Names.KerName.repr kn in
     let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
     print_list pr_id qn
   in
@@ -265,8 +265,8 @@ let print_namespace ns =
   let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
   let constants_in_namespace =
     Cmap_env.fold (fun c (body,_) acc ->
-      let kn = user_con c in
-      if matches (modpath kn) then
+      let kn = Constant.user c in
+      if matches (KerName.modpath kn) then
         acc++fnl()++hov 2 (print_constant kn body)
       else
         acc