Modulification of name

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

1 files changed, 22 insertions, 22 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 17c55f069..b20e0a1d0 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 *)