24 files changed, 77 insertions, 77 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index fca402c58..b7ecb2461 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -15,7 +15,7 @@ open Util
 open Libobject
 (*i*)
 
-let empty_name_table = (Refmap.empty : name list list Refmap.t)
+let empty_name_table = (Refmap.empty : Name.t list list Refmap.t)
 let name_table = ref empty_name_table
 
 let _ =
@@ -26,7 +26,7 @@ let _ =
 
 type req =
   | ReqLocal
-  | ReqGlobal of global_reference * name list list
+  | ReqGlobal of global_reference * Name.t list list
 
 let load_rename_args _ (_, (_, (r, names))) =
   name_table := Refmap.add r names !name_table
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index 1b1f7576d..09b8859e6 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -11,10 +11,10 @@ open Globnames
 open Environ
 open Term
 
-val rename_arguments : bool -> global_reference -> name list list -> unit
+val rename_arguments : bool -> global_reference -> Name.t list list -> unit
 
 (** [Not_found] is raised is no names are defined for [r] *)
-val arguments_names : global_reference -> name list list
+val arguments_names : global_reference -> Name.t list list
 
 val rename_type_of_constant : env -> constant -> types
 val rename_type_of_inductive : env -> inductive -> types
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 17fb5503c..71c9325d7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -114,7 +114,7 @@ type 'a rhs =
 type 'a equation =
     { patterns     : cases_pattern list;
       rhs          : 'a rhs;
-      alias_stack  : name list;
+      alias_stack  : Name.t list;
       eqn_loc      : Loc.t;
       used         : bool ref }
 
@@ -122,12 +122,12 @@ type 'a matrix = 'a equation list
 
 (* 1st argument of IsInd is the original ind before extracting the summary *)
 type tomatch_type =
-  | IsInd of types * inductive_type * name list
+  | IsInd of types * inductive_type * Name.t list
   | NotInd of constr option * types
 
 type tomatch_status =
-  | Pushed of ((constr * tomatch_type) * int list * name)
-  | Alias of (name * constr * (constr * types))
+  | Pushed of ((constr * tomatch_type) * int list * Name.t)
+  | Alias of (Name.t * constr * (constr * types))
   | NonDepAlias
   | Abstract of int * rel_declaration
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d1ca69dcd..d9f9b9d76 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -74,7 +74,7 @@ type 'a rhs =
 type 'a equation =
     { patterns     : cases_pattern list;
       rhs          : 'a rhs;
-      alias_stack  : name list;
+      alias_stack  : Name.t list;
       eqn_loc      : Loc.t;
       used         : bool ref }
 
@@ -82,12 +82,12 @@ type 'a matrix = 'a equation list
 
 (* 1st argument of IsInd is the original ind before extracting the summary *)
 type tomatch_type =
-  | IsInd of types * inductive_type * name list
+  | IsInd of types * inductive_type * Name.t list
   | NotInd of constr option * types
 
 type tomatch_status =
-  | Pushed of ((constr * tomatch_type) * int list * name)
-  | Alias of (name * constr * (constr * types))
+  | Pushed of ((constr * tomatch_type) * int list * Name.t)
+  | Alias of (Name.t * constr * (constr * types))
   | NonDepAlias
   | Abstract of int * rel_declaration
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index cb71e1aa6..a84bbcc54 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -41,7 +41,7 @@ type cbv_value =
   | VAL of int * constr
   | STACK of int * cbv_value * cbv_stack
   | CBN of constr * cbv_value subs
-  | LAM of int * (name * constr) list * constr * cbv_value subs
+  | LAM of int * (Name.t * constr) list * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor * cbv_value array
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 08e52ff72..66aef4d14 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -27,7 +27,7 @@ type cbv_value =
   | VAL of int * constr
   | STACK of int * cbv_value * cbv_stack
   | CBN of constr * cbv_value subs
-  | LAM of int * (name * constr) list * constr * cbv_value subs
+  | LAM of int * (Name.t * constr) list * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value array
   | COFIXP of cofixpoint * cbv_value subs * cbv_value array
   | CONSTR of constructor * cbv_value array
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 001f3b5a6..d9d82faa2 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -323,7 +323,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
               | GLambda (_,x,_,t,c) -> x, c
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
-	      if List.for_all (name_eq Anonymous) nl then None
+	      if List.for_all (Name.equal Anonymous) nl then None
 	      else Some (dl,indsp,nl) in
             n, aliastyp, Some typ
   in
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 1e31e04d4..3a8f54904 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -54,7 +54,7 @@ val synthetize_type : unit -> bool
 
 (** Utilities to transform kernel cases to simple pattern-matching problem *)
 
-val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_constr
+val it_destRLambda_or_LetIn_names : int -> glob_constr -> Name.t list * glob_constr
 val simple_cases_matrix_of_branches :
   inductive -> (int * int * glob_constr) list -> cases_clauses
 val return_type_of_predicate :
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index b056cd260..9c6f1ad47 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -157,7 +157,7 @@ val mk_valcon : constr -> val_constraint
 
 val split_tycon :
   Loc.t -> env ->  evar_map -> type_constraint ->
-    evar_map * (name * type_constraint * type_constraint)
+    evar_map * (Name.t * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint
 val lift_tycon : int -> type_constraint -> type_constraint
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 8722516bb..4c18aec19 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -294,8 +294,8 @@ type instance_status = instance_constraint * instance_typing_status
 (* Clausal environments *)
 
 type clbinding =
-  | Cltyp of name * constr freelisted
-  | Clval of name * (constr freelisted * instance_status) * constr freelisted
+  | Cltyp of Name.t * constr freelisted
+  | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
 
 let map_clb f = function
   | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl)
@@ -650,7 +650,7 @@ let meta_with_name evd id =
     Metamap.fold
       (fun n clb (l1,l2 as l) ->
         let (na',def) = clb_name clb in
-        if name_eq na na' then if def then (n::l1,l2) else (n::l1,n::l2)
+        if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
         else l)
       evd.metas ([],[]) in
   match mvnodef, mvl with
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a73dbdcdc..86ec47d3e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -68,8 +68,8 @@ type instance_status = instance_constraint * instance_typing_status
 (** Clausal environments *)
 
 type clbinding =
-  | Cltyp of name * constr freelisted
-  | Clval of name * (constr freelisted * instance_status) * constr freelisted
+  | Cltyp of Name.t * constr freelisted
+  | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
 
 val map_clb : (constr -> constr) -> clbinding -> clbinding
 
@@ -216,10 +216,10 @@ val meta_fvalue    : evar_map -> metavariable -> constr freelisted * instance_st
 val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option
 val meta_type      : evar_map -> metavariable -> types
 val meta_ftype     : evar_map -> metavariable -> types freelisted
-val meta_name      : evar_map -> metavariable -> name
+val meta_name      : evar_map -> metavariable -> Name.t
 val meta_with_name : evar_map -> Id.t -> metavariable
 val meta_declare   :
-  metavariable -> types -> ?name:name -> evar_map -> evar_map
+  metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
 val meta_assign    : metavariable -> constr * instance_status -> evar_map -> evar_map
 val meta_reassign  : metavariable -> constr * instance_status -> evar_map -> evar_map
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 2e8908cfb..730332514 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -24,7 +24,7 @@ val glob_sort_eq : glob_sort -> glob_sort -> bool
 
 val cases_pattern_loc : cases_pattern -> Loc.t
 
-val cases_predicate_names : tomatch_tuples -> name list
+val cases_predicate_names : tomatch_tuples -> Name.t list
 
 (** Apply one argument to a glob_constr *)
 val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr
@@ -46,6 +46,6 @@ val loc_of_glob_constr : glob_constr -> Loc.t
 
     Take the current alias as parameter,
     @raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
+val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 
-val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
+val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index cbfd78deb..8009524de 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -291,7 +291,7 @@ let next_name_away_for_default_printing env_t na avoid =
 type renaming_flags =
   | RenamingForCasesPattern
   | RenamingForGoal
-  | RenamingElsewhereFor of (name list * constr)
+  | RenamingElsewhereFor of (Name.t list * constr)
 
 let next_name_for_display flags =
   match flags with
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 6702c9f70..6c982451a 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -16,15 +16,15 @@ open Environ
 val lowercase_first_char : Id.t -> string
 val sort_hdchar : sorts -> string
 val hdchar : env -> types -> string
-val id_of_name_using_hdchar : env -> types -> name -> Id.t
-val named_hd : env -> types -> name -> name
+val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t
+val named_hd : env -> types -> Name.t -> Name.t
 
-val mkProd_name : env -> name * types * types -> types
-val mkLambda_name : env -> name * types * constr -> constr
+val mkProd_name : env -> Name.t * types * types -> types
+val mkLambda_name : env -> Name.t * types * constr -> constr
 
 (** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> name * types * types -> types
-val lambda_name : env -> name * types * constr -> constr
+val prod_name : env -> Name.t * types * types -> types
+val lambda_name : env -> Name.t * types * constr -> constr
 
 val prod_create : env -> types * types -> constr
 val lambda_create : env -> types * constr -> constr
@@ -53,16 +53,16 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
 val next_global_ident_away : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a constructor name already used in current module *)
-val next_name_away_in_cases_pattern : name -> Id.t list -> Id.t
+val next_name_away_in_cases_pattern : Name.t -> Id.t list -> Id.t
 
-val next_name_away  : name -> Id.t list -> Id.t (** default is "H" *)
-val next_name_away_with_default : string -> name -> Id.t list ->
+val next_name_away  : Name.t -> Id.t list -> Id.t (** default is "H" *)
+val next_name_away_with_default : string -> Name.t -> Id.t list ->
   Id.t
 
-val next_name_away_with_default_using_types : string -> name ->
+val next_name_away_with_default_using_types : string -> Name.t ->
   Id.t list -> types -> Id.t
 
-val set_reserved_typed_name : (types -> name) -> unit
+val set_reserved_typed_name : (types -> Name.t) -> unit
 
 (*********************************************************************
    Making name distinct for displaying *)
@@ -70,15 +70,15 @@ val set_reserved_typed_name : (types -> name) -> unit
 type renaming_flags =
   | RenamingForCasesPattern (** avoid only global constructors *)
   | RenamingForGoal (** avoid all globals (as in intro) *)
-  | RenamingElsewhereFor of (name list * constr)
+  | RenamingElsewhereFor of (Name.t list * constr)
 
 val make_all_name_different : env -> env
 
 val compute_displayed_name_in :
-  renaming_flags -> Id.t list -> name -> constr -> name * Id.t list
+  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_and_force_displayed_name_in :
-  renaming_flags -> Id.t list -> name -> constr -> name * Id.t list
+  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val compute_displayed_let_name_in :
-  renaming_flags -> Id.t list -> name -> constr -> name * Id.t list
+  renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
 val rename_bound_vars_as_displayed :
-  Id.t list -> name list -> types -> types
+  Id.t list -> Name.t list -> types -> types
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d784fc0ed..c1e91ca2f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -39,11 +39,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PSoApp (id1, arg1), PSoApp (id2, arg2) ->
   Id.equal id1 id2 && List.equal constr_pattern_eq arg1 arg2
 | PLambda (v1, t1, b1), PLambda (v2, t2, b2) ->
-  name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PProd (v1, t1, b1), PProd (v2, t2, b2) ->
-  name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
-  name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PSort s1, PSort s2 -> glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
@@ -73,7 +73,7 @@ and cofixpoint_eq (i1, r1) (i2, r2) =
   rec_declaration_eq r1 r2
 
 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
-  Array.equal name_eq n1 n2 &&
+  Array.equal Name.equal n1 n2 &&
   Array.equal eq_constr c1 c2 &&
   Array.equal eq_constr r1 r2
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cced783f5..ad6922dbe 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -28,9 +28,9 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
   | CannotFindWellTypedAbstraction of constr * constr list
-  | WrongAbstractionType of name * constr * types * types
-  | AbstractionOverMeta of name * name
-  | NonLinearUnification of name * constr
+  | WrongAbstractionType of Name.t * constr * types * types
+  | AbstractionOverMeta of Name.t * Name.t
+  | NonLinearUnification of Name.t * constr
   (* Pretyping *)
   | VarNotFound of Id.t
   | UnexpectedType of constr * constr
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index aa0b65e4f..558f3d5bb 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -30,9 +30,9 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
   | CannotFindWellTypedAbstraction of constr * constr list
-  | WrongAbstractionType of name * constr * types * types
-  | AbstractionOverMeta of name * name
-  | NonLinearUnification of name * constr
+  | WrongAbstractionType of Name.t * constr * types * types
+  | AbstractionOverMeta of Name.t * Name.t
+  | NonLinearUnification of Name.t * constr
   (** Pretyping *)
   | VarNotFound of Id.t
   | UnexpectedType of constr * constr
@@ -82,7 +82,7 @@ val error_number_branches_loc :
 
 val error_ill_typed_rec_body_loc :
   Loc.t -> env -> Evd.evar_map ->
-      int -> name array -> unsafe_judgment array -> types array -> 'b
+      int -> Name.t array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
   Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
@@ -108,7 +108,7 @@ val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
       constr -> constr list -> 'b
 
 val error_wrong_abstraction_type :  env -> Evd.evar_map ->
-      name -> constr -> types -> types -> 'b
+      Name.t -> constr -> types -> types -> 'b
 
 val error_abstraction_over_meta : env -> Evd.evar_map ->
   metavariable -> metavariable -> 'b
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 72d43fabd..777e6c1d8 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -36,7 +36,7 @@ open Reductionops
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (name * bool) list;
+  s_PROJKIND : (Name.t * bool) list;
   s_PROJ : constant option list }
 
 let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
@@ -46,7 +46,7 @@ let projection_table = ref Cmap.empty
    is the inductive always (fst constructor) ? It seems so... *)
 
 type struc_tuple =
-    inductive * constructor * (name * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * constant option list
 
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 538e6d540..6afba15bf 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -22,11 +22,11 @@ open Library
 type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : (name * bool) list;
+  s_PROJKIND : (Name.t * bool) list;
   s_PROJ : constant option list }
 
 type struc_tuple =
-    inductive * constructor * (name * bool) list * constant option list
+    inductive * constructor * (Name.t * bool) list * constant option list
 
 val declare_structure : struc_tuple -> unit
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 4263aec53..60c111370 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -154,9 +154,9 @@ val hnf_lam_app      : env ->  evar_map -> constr -> constr -> constr
 val hnf_lam_appvect  : env ->  evar_map -> constr -> constr array -> constr
 val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
-val splay_prod : env ->  evar_map -> constr -> (name * constr) list * constr
-val splay_lam : env ->  evar_map -> constr -> (name * constr) list * constr
-val splay_arity : env ->  evar_map -> constr -> (name * constr) list * sorts
+val splay_prod : env ->  evar_map -> constr -> (Name.t * constr) list * constr
+val splay_lam : env ->  evar_map -> constr -> (Name.t * constr) list * constr
+val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * sorts
 val sort_of_arity : env -> evar_map -> constr -> sorts
 val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f48734be7..f5be89689 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -838,7 +838,7 @@ let add_vname vars = function
 (*************************)
 (*   Names environments  *)
 (*************************)
-type names_context = name list
+type names_context = Name.t list
 let add_name n nl = n::nl
 let lookup_name_of_rel p names =
   try List.nth names (p-1)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 051a77883..3e0f0e0eb 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -37,9 +37,9 @@ val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
 (** about contexts *)
-val push_rel_assum : name * types -> env -> env
-val push_rels_assum : (name * types) list -> env -> env
-val push_named_rec_types : name array * types array * 'a -> env -> env
+val push_rel_assum : Name.t * types -> env -> env
+val push_rels_assum : (Name.t * types) list -> env -> env
+val push_named_rec_types : Name.t array * types array * 'a -> env -> env
 
 val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
 (** Associates the contents of an identifier in a [rel_context]. Raise
@@ -54,8 +54,8 @@ val extended_rel_vect : int -> rel_context -> constr array
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
 val mkProd_wo_LetIn : rel_declaration -> types -> types
-val it_mkProd : types -> (name * types) list -> types
-val it_mkLambda : constr -> (name * types) list -> constr
+val it_mkProd : types -> (Name.t * types) list -> types
+val it_mkLambda : constr -> (Name.t * types) list -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types
 val it_mkProd_wo_LetIn : types -> rel_context -> types
 val it_mkLambda_or_LetIn : constr -> rel_context -> constr
@@ -69,7 +69,7 @@ val it_named_context_quantifier :
 (** {6 Generic iterators on constr} *)
 
 val map_constr_with_named_binders :
-  (name -> 'a -> 'a) ->
+  (Name.t -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 val map_constr_with_binders_left_to_right :
   (rel_declaration -> 'a -> 'a) ->
@@ -225,9 +225,9 @@ val adjust_app_array_size : constr -> constr array -> constr -> constr array ->
   (constr * constr array * constr * constr array)
 
 (** name contexts *)
-type names_context = name list
-val add_name : name -> names_context -> names_context
-val lookup_name_of_rel : int -> names_context -> name
+type names_context = Name.t list
+val add_name : Name.t -> names_context -> names_context
+val lookup_name_of_rel : int -> names_context -> Name.t
 val lookup_rel_of_name : Id.t -> names_context -> int
 val empty_names_context : names_context
 val ids_of_rel_context : rel_context -> Id.t list
@@ -240,11 +240,11 @@ val env_rel_context_chop : int -> env -> env * rel_context
 
 (** Set of local names *)
 val vars_of_env: env -> Id.Set.t
-val add_vname : Id.Set.t -> name -> Id.Set.t
+val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 
 (** other signature iterators *)
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
-val assums_of_rel_context : rel_context -> (name * constr) list
+val assums_of_rel_context : rel_context -> (Name.t * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val substl_rel_context : constr list -> rel_context -> rel_context
 val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b5c710da2..0fe13ef9c 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -58,7 +58,7 @@ type typeclass = {
   cl_props : rel_context;
 
   (* The method implementaions as projections. *)
-  cl_projs : (name * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * int option) option * constant option) list;
 }
 
 module Gmap = Fmap.Make(RefOrdered)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 72b3bbd27..5e2b9b78d 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -37,7 +37,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 * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * int option) option * constant option) list;
 }
 
 type instance