Modulification of name

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 120 insertions, 86 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 934701f43c..1630cff38b 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -335,9 +335,9 @@ and fterm =
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
-  | 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 * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
diff --git a/kernel/closure.mli b/kernel/closure.mli
index d7a775fdef..3a9603a370 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -111,9 +111,9 @@ type fterm =
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCases of case_info * fconstr * fconstr * fconstr array
-  | 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 * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
@@ -157,7 +157,7 @@ val mk_atom : 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/kernel/declarations.ml b/kernel/declarations.ml
index 6b793ce2f5..bc721dce34 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -136,7 +136,7 @@ let subst_const_body sub cb = {
 (* Hash-consing of [constant_body] *)
 
 let hcons_rel_decl ((n,oc,t) as d) =
-  let n' = hcons_name n
+  let n' = Name.hcons n
   and oc' = Option.smartmap hcons_constr oc
   and t' = hcons_types t
   in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
diff --git a/kernel/modops.ml b/kernel/modops.ml
index e7afec2a05..e135866899 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -39,7 +39,7 @@ type signature_mismatch_error =
   | InductiveNumbersFieldExpected of int
   | InductiveParamsNumberField of int
   | RecordFieldExpected of bool
-  | RecordProjectionsExpected of name list
+  | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index c90425fd73..cfd8394569 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -66,7 +66,7 @@ type signature_mismatch_error =
   | InductiveNumbersFieldExpected of int
   | InductiveParamsNumberField of int
   | RecordFieldExpected of bool
-  | RecordProjectionsExpected of name list
+  | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
 
diff --git a/kernel/names.ml b/kernel/names.ml
index c6f5f891cb..12df0a3c8e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -74,16 +74,46 @@ struct
 
 end
 
+
+module Name =
+struct
+  type t = Name of Id.t | Anonymous
+
+  let equal n1 n2 = match n1, n2 with
+  | Anonymous, Anonymous -> true
+  | Name id1, Name id2 -> String.equal id1 id2
+  | _ -> false
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = Id.t -> Id.t
+      let hashcons hident = function
+        | Name id -> Name (hident id)
+        | n -> n
+      let equal n1 n2 =
+        n1 == n2 ||
+        match (n1,n2) with
+          | (Name id1, Name id2) -> id1 == id2
+          | (Anonymous,Anonymous) -> true
+          | _ -> false
+      let hash = Hashtbl.hash
+    end
+
+  module Hname = Hashcons.Make(Self_Hashcons)
+
+  let hcons = Hashcons.simple_hcons Hname.generate Id.hcons
+
+end
+
+type name = Name.t = Name of Id.t | Anonymous
+(** Alias, to import constructors. *)
+
 (** {6 Various types based on identifiers } *)
 
-type name = Name of Id.t | Anonymous
 type variable = Id.t
 
-let name_eq n1 n2 = match n1, n2 with
-| Anonymous, Anonymous -> true
-| Name id1, Name id2 -> String.equal id1 id2
-| _ -> false
-
 type module_ident = Id.t
 
 module ModIdmap = Id.Map
@@ -448,22 +478,6 @@ let eq_egr e1 e2 = match e1, e2 with
 
 (** {6 Hash-consing of name objects } *)
 
-module Hname = Hashcons.Make(
-  struct
-    type t = name
-    type u = Id.t -> Id.t
-    let hashcons hident = function
-      | Name id -> Name (hident id)
-      | n -> n
-    let equal n1 n2 =
-      n1 == n2 ||
-      match (n1,n2) with
-	| (Name id1, Name id2) -> id1 == id2
-        | (Anonymous,Anonymous) -> true
-        | _ -> false
-    let hash = Hashtbl.hash
-  end)
-
 module Hmod = Hashcons.Make(
   struct
     type t = module_path
@@ -526,7 +540,6 @@ module Hconstruct = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-let hcons_name = Hashcons.simple_hcons Hname.generate Id.hcons
 let hcons_mp =
   Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,MBId.hcons,String.hcons)
 let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons)
@@ -631,3 +644,9 @@ let label_of_id = Label.of_id
 let eq_label = Label.equal
 
 (** / End of compatibility layer for [Label] *)
+
+(** Compatibility layer for [Name] *)
+
+let name_eq = Name.equal
+
+(** / End of compatibility layer for [Name] *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 947b9e3fde..a51ac0ad86 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -55,14 +55,25 @@ sig
 
 end
 
-(** {6 Various types based on identifiers } *)
+module Name :
+sig
+  type t = Name of Id.t | Anonymous
+  (** A name is either undefined, either an identifier. *)
+
+  val equal : t -> t -> bool
+  (** Equality over names. *)
+
+  val hcons : t -> t
+  (** Hashconsing over names. *)
 
-type name = Name of Id.t | Anonymous
+end
+
+(** {6 Type aliases} *)
+
+type name = Name.t = Name of Id.t | Anonymous
 type variable = Id.t
 type module_ident = Id.t
 
-val name_eq : name -> name -> bool
-
 (** {6 Directory paths = section names paths } *)
 
 module Dir_path :
@@ -100,8 +111,6 @@ sig
 
 end
 
-module ModIdmap : Map.S with type key = module_ident
-
 (** {6 Names of structure elements } *)
 
 module Label :
@@ -164,6 +173,8 @@ sig
 
 end
 
+module ModIdmap : Map.S with type key = module_ident
+
 (** {6 The module part of the kernel name } *)
 
 type module_path =
@@ -290,7 +301,6 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 
 (** {6 Hash-consing } *)
 
-val hcons_name : name -> name
 val hcons_con : constant -> constant
 val hcons_mind : mutual_inductive -> mutual_inductive
 val hcons_ind : inductive -> inductive
@@ -439,3 +449,8 @@ val string_of_mbid : mod_bound_id -> string
 
 val debug_string_of_mbid : mod_bound_id -> string
 (** @deprecated Same as [MBId.debug_to_string]. *)
+
+(** {5 Names} *)
+
+val name_eq : name -> name -> bool
+(** @deprecated Same as [Name.equal]. *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c15681b043..11ae7c8633 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -198,7 +198,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     check (fun mib ->
       let nparamdecls = List.length mib.mind_params_ctxt in
       let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
-      snd (List.chop nparamdecls names)) (List.equal name_eq)
+      snd (List.chop nparamdecls names)) (List.equal Name.equal)
       (fun x -> RecordProjectionsExpected x);
   end;
   (* we first check simple things *)
diff --git a/kernel/term.ml b/kernel/term.ml
index ced5c6fc5e..9cb38e33da 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -95,7 +95,7 @@ let family_of_sort = function
    the same order (i.e. last argument first) *)
 type 'constr pexistential = existential_key * 'constr array
 type ('constr, 'types) prec_declaration =
-    name array * 'types array * 'constr array
+    Name.t array * 'types array * 'constr array
 type ('constr, 'types) pfixpoint =
     (int array * int) * ('constr, 'types) prec_declaration
 type ('constr, 'types) pcofixpoint =
@@ -110,9 +110,9 @@ type ('constr, 'types) kind_of_term =
   | Evar      of 'constr pexistential
   | Sort      of sorts
   | Cast      of 'constr * cast_kind * 'types
-  | Prod      of name * 'types * 'types
-  | Lambda    of name * 'types * 'constr
-  | LetIn     of name * 'constr * 'types * 'constr
+  | Prod      of Name.t * 'types * 'types
+  | Lambda    of Name.t * 'types * 'constr
+  | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
   | Const     of constant
   | Ind       of inductive
@@ -126,7 +126,7 @@ type ('constr, 'types) kind_of_term =
 type constr = (constr,constr) kind_of_term
 
 type existential = existential_key * constr array
-type rec_declaration = name array * constr array * constr array
+type rec_declaration = Name.t array * constr array * constr array
 type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
 
@@ -250,8 +250,8 @@ let kind_of_term c = c
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
   | CastType   of 'types * 'types
-  | ProdType   of name * 'types * 'types
-  | LetInType  of name * 'constr * 'types * 'types
+  | ProdType   of Name.t * 'types * 'types
+  | LetInType  of Name.t * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
 
 let kind_of_type = function
@@ -670,7 +670,7 @@ type types = constr
 type strategy = types option
 
 type named_declaration = Id.t * constr option * types
-type rel_declaration = name * constr option * types
+type rel_declaration = Name.t * constr option * types
 
 let map_named_declaration f (id, (v : strategy), ty) = (id, Option.map f v, f ty)
 let map_rel_declaration = map_named_declaration
@@ -688,7 +688,7 @@ let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
   Id.equal i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
 
 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
-  name_eq n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
+  Name.equal n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
 
 (***************************************************************************)
 (*     Type of local contexts (telescopes)                                 *)
@@ -1432,7 +1432,7 @@ let hcons_constr =
      hcons_construct,
      hcons_ind,
      hcons_con,
-     hcons_name,
+     Name.hcons,
      Id.hcons)
 
 let hcons_types = hcons_constr
diff --git a/kernel/term.mli b/kernel/term.mli
index 17c55f0699..b20e0a1d08 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -103,7 +103,7 @@ type cast_kind = VMcast | DEFAULTcast | REVERTcast
 val mkCast : constr * cast_kind * constr -> constr
 
 (** Constructs the product [(x:t1)t2] *)
-val mkProd : name * types * types -> types
+val mkProd : Name.t * types * types -> types
 val mkNamedProd : Id.t -> types -> types -> types
 
 (** non-dependent product [t1 -> t2], an alias for
@@ -113,11 +113,11 @@ val mkNamedProd : Id.t -> types -> types -> types
 val mkArrow : types -> types -> constr
 
 (** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)
-val mkLambda : name * types * constr -> constr
+val mkLambda : Name.t * types * constr -> constr
 val mkNamedLambda : Id.t -> types -> constr -> constr
 
 (** Constructs the product [let x = t1 : t2 in t3] *)
-val mkLetIn : name * constr * types * constr -> constr
+val mkLetIn : Name.t * constr * types * constr -> constr
 val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 
 (** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
@@ -164,7 +164,7 @@ val mkCase : case_info * constr * constr * constr array -> constr
 
    where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
 *)
-type rec_declaration = name array * types array * constr array
+type rec_declaration = Name.t array * types array * constr array
 type fixpoint = (int array * int) * rec_declaration
 val mkFix : fixpoint -> constr
 
@@ -189,7 +189,7 @@ val mkCoFix : cofixpoint -> constr
    the same order (i.e. last argument first) *)
 type 'constr pexistential = existential_key * 'constr array
 type ('constr, 'types) prec_declaration =
-    name array * 'types array * 'constr array
+    Name.t array * 'types array * 'constr array
 type ('constr, 'types) pfixpoint =
     (int array * int) * ('constr, 'types) prec_declaration
 type ('constr, 'types) pcofixpoint =
@@ -202,9 +202,9 @@ type ('constr, 'types) kind_of_term =
   | Evar      of 'constr pexistential
   | Sort      of sorts
   | Cast      of 'constr * cast_kind * 'types
-  | Prod      of name * 'types * 'types
-  | Lambda    of name * 'types * 'constr
-  | LetIn     of name * 'constr * 'types * 'constr
+  | Prod      of Name.t * 'types * 'types
+  | Lambda    of Name.t * 'types * 'constr
+  | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
   | Const     of constant
   | Ind       of inductive
@@ -223,8 +223,8 @@ val kind_of_term : constr -> (constr, types) kind_of_term
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
   | CastType   of 'types * 'types
-  | ProdType   of name * 'types * 'types
-  | LetInType  of name * 'constr * 'types * 'types
+  | ProdType   of Name.t * 'types * 'types
+  | LetInType  of Name.t * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
 
 val kind_of_type : types -> (constr, types) kind_of_type
@@ -281,13 +281,13 @@ val destSort : constr -> sorts
 val destCast : constr -> constr * cast_kind * constr
 
 (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
-val destProd : types -> name * types * types
+val destProd : types -> Name.t * types * types
 
 (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
-val destLambda : constr -> name * types * constr
+val destLambda : constr -> Name.t * types * constr
 
 (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
-val destLetIn : constr -> name * constr * types * constr
+val destLetIn : constr -> Name.t * constr * types * constr
 
 (** Destructs an application *)
 val destApp : constr -> constr * constr array
@@ -338,7 +338,7 @@ val destCoFix : constr -> cofixpoint
     purpose) *)
 
 type named_declaration = Id.t * constr option * types
-type rel_declaration = name * constr option * types
+type rel_declaration = Name.t * constr option * types
 
 val map_named_declaration :
   (constr -> constr) -> named_declaration -> named_declaration
@@ -399,24 +399,24 @@ val appvectc : constr -> constr array -> constr
 
 (** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b]
    where [l] is [(x_n,T_n)...(x_1,T_1)...]. *)
-val prodn : int -> (name * constr) list -> constr -> constr
+val prodn : int -> (Name.t * constr) list -> constr -> constr
 
 (** [compose_prod l b]
    @return [forall (x_1:T_1)...(x_n:T_n), b]
    where [l] is [(x_n,T_n)...(x_1,T_1)].
    Inverse of [decompose_prod]. *)
-val compose_prod : (name * constr) list -> constr -> constr
+val compose_prod : (Name.t * constr) list -> constr -> constr
 
 (** [lamn n l b]
     @return [fun (x_1:T_1)...(x_n:T_n) => b]
    where [l] is [(x_n,T_n)...(x_1,T_1)...]. *)
-val lamn : int -> (name * constr) list -> constr -> constr
+val lamn : int -> (Name.t * constr) list -> constr -> constr
 
 (** [compose_lam l b]
    @return [fun (x_1:T_1)...(x_n:T_n) => b]
    where [l] is [(x_n,T_n)...(x_1,T_1)].
    Inverse of [it_destLam] *)
-val compose_lam : (name * constr) list -> constr -> constr
+val compose_lam : (Name.t * constr) list -> constr -> constr
 
 (** [to_lambda n l]
    @return [fun (x_1:T_1)...(x_n:T_n) => T]
@@ -441,20 +441,20 @@ val it_mkProd_or_LetIn : types -> rel_context -> types
 
 (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *)
-val decompose_prod : constr -> (name*constr) list * constr
+val decompose_prod : constr -> (Name.t*constr) list * constr
 
 (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
-val decompose_lam : constr -> (name*constr) list * constr
+val decompose_lam : constr -> (Name.t*constr) list * constr
 
 (** Given a positive integer n, transforms a product term
    {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
    into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
-val decompose_prod_n : int -> constr -> (name * constr) list * constr
+val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
    {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
-val decompose_lam_n : int -> constr -> (name * constr) list * constr
+val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 6d4b420262..4c2799df8c 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -48,14 +48,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * constructor * constr * constr
-  | Generalization of (name * types) * unsafe_judgment
+  | Generalization of (Name.t * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array
+  | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * types array
+      int * Name.t array * unsafe_judgment array * types array
 
 exception TypeError of env * type_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 1967018f69..531ad0b9ee 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -49,14 +49,14 @@ type type_error =
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
   | IllFormedBranch of constr * constructor * constr * constr
-  | Generalization of (name * types) * unsafe_judgment
+  | Generalization of (Name.t * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array
+  | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array
   | IllTypedRecBody of
-      int * name array * unsafe_judgment array * types array
+      int * Name.t array * unsafe_judgment array * types array
 
 exception TypeError of env * type_error
 
@@ -80,7 +80,7 @@ val error_number_branches : env -> unsafe_judgment -> int -> 'a
 
 val error_ill_formed_branch : env -> constr -> constructor -> constr -> constr -> 'a
 
-val error_generalization : env -> name * types -> unsafe_judgment -> 'a
+val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
 
 val error_actual_type : env -> unsafe_judgment -> types -> 'a
 
@@ -92,9 +92,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 -> env -> unsafe_judgment array -> 'a
+  env -> guard_error -> Name.t array -> int -> env -> unsafe_judgment array -> 'a
 
 val error_ill_typed_rec_body  :
-  env -> int -> name array -> unsafe_judgment array -> types array -> 'a
+  env -> int -> Name.t array -> unsafe_judgment array -> types array -> 'a
 
 val error_elim_explain : sorts_family -> sorts_family -> arity_error
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 7b3aff20dc..7617e82195 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -56,17 +56,17 @@ val judge_of_apply :
 
 (** {6 Type of an abstraction. } *)
 val judge_of_abstraction :
-  env -> name -> unsafe_type_judgment -> unsafe_judgment
+  env -> Name.t -> unsafe_type_judgment -> unsafe_judgment
     -> unsafe_judgment
 
 (** {6 Type of a product. } *)
 val judge_of_product :
-  env -> name -> unsafe_type_judgment -> unsafe_type_judgment
+  env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment
     -> unsafe_judgment
 
 (** s Type of a let in. *)
 val judge_of_letin :
-  env -> name -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment
+  env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment
     -> unsafe_judgment
 
 (** {6 Type of a cast. } *)
@@ -89,7 +89,7 @@ val judge_of_case : env -> case_info
     -> unsafe_judgment * constraints
 
 (** Typecheck general fixpoint (not checking guard conditions) *)
-val type_fixpoint : env -> name array -> types array
+val type_fixpoint : env -> Name.t array -> types array
     -> unsafe_judgment array -> constraints
 
 (** Kernel safe typing but applicable to partial proofs *)