Modulification of name

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

9 files changed, 31 insertions, 31 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index e9dae6421b..28faa2ce6a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -109,7 +109,7 @@ let rec constr_expr_eq e1 e2 =
       List.equal binder_expr_eq bl1 bl2 &&
       constr_expr_eq a1 a2
   | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) ->
-      name_eq na1 na2 &&
+      Name.equal na1 na2 &&
       constr_expr_eq a1 a2 &&
       constr_expr_eq b1 b2
   | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) ->
@@ -132,14 +132,14 @@ let rec constr_expr_eq e1 e2 =
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
   | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) ->
-    List.equal (eq_located name_eq) n1 n2 &&
-    Option.equal (eq_located name_eq) m1 m2 &&
+    List.equal (eq_located Name.equal) n1 n2 &&
+    Option.equal (eq_located Name.equal) m1 m2 &&
     Option.equal constr_expr_eq e1 e2 &&
     constr_expr_eq t1 t2 &&
     constr_expr_eq b1 b2
   | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) ->
     constr_expr_eq e1 e2 &&
-    Option.equal (eq_located name_eq) n1 n2 &&
+    Option.equal (eq_located Name.equal) n1 n2 &&
     Option.equal constr_expr_eq r1 r2 &&
     constr_expr_eq t1 t2 &&
     constr_expr_eq f1 f2
@@ -176,7 +176,7 @@ and args_eq (a1,e1) (a2,e2) =
 
 and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
   constr_expr_eq e1 e2 &&
-  Option.equal (eq_located name_eq) n1 n2 &&
+  Option.equal (eq_located Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
 
 and branch_expr_eq (_, p1, e1) (_, p2, e2) =
@@ -185,7 +185,7 @@ and branch_expr_eq (_, p1, e1) (_, p2, e2) =
 
 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
   (** Don't care about the [binder_kind] *)
-  List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2
+  List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
 
 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
   (eq_located Id.equal id1 id2) &&
@@ -210,10 +210,10 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
 
 and local_binder_eq l1 l2 = match l1, l2 with
 | LocalRawDef (n1, e1), LocalRawDef (n2, e2) ->
-  eq_located name_eq n1 n2 && constr_expr_eq e1 e2
+  eq_located Name.equal n1 n2 && constr_expr_eq e1 e2
 | LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) ->
   (** Don't care about the [binder_kind] *)
-  List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2
+  List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
 | _ -> false
 
 and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 49dea9f312..d857a5b604 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -48,9 +48,9 @@ val mkIdentC : Id.t -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
 val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
-val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr
+val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
@@ -69,17 +69,17 @@ val coerce_reference_to_id : reference -> Id.t
 val coerce_to_id : constr_expr -> Id.t located
 (** Destruct terms of the form [CRef (Ident _)]. *)
 
-val coerce_to_name : constr_expr -> name located
+val coerce_to_name : constr_expr -> Name.t located
 (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
 
 (** {6 Binder manipulation} *)
 
 val default_binder_kind : binder_kind
 
-val names_of_local_binders : local_binder list -> name located list
+val names_of_local_binders : local_binder list -> Name.t located list
 (** Retrieve a list of binding names from a list of binders. *)
 
-val names_of_local_assums : local_binder list -> name located list
+val names_of_local_assums : local_binder list -> Name.t located list
 (** Same as [names_of_local_binders], but does not take the [let] bindings into
     account. *)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8d44bc5317..a4a74059e4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -66,7 +66,7 @@ type var_internalization_data =
 type internalization_env =
     (var_internalization_data) Id.Map.t
 
-type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
+type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
 let interning_grammar = ref false
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0e4d0c6510..83cc1dcad0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -70,7 +70,7 @@ val compute_internalization_env : env -> var_internalization_type ->
 
 type ltac_sign = Id.t list * unbound_ltac_var_map
 
-type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
+type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
 (** {6 Internalization performs interpretation of global names and notations } *)
 
@@ -148,9 +148,9 @@ val interp_reference : ltac_sign -> reference -> glob_constr
 
 (** Interpret binders *)
 
-val interp_binder  : evar_map -> env -> name -> constr_expr -> types
+val interp_binder  : evar_map -> env -> Name.t -> constr_expr -> types
 
-val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
+val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types
 
 (** Interpret contexts: returns extended env and context *)
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 2c5ad7408f..66be2ae5a3 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -34,23 +34,23 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
   Id.t list -> Id.t list
 
 val free_vars_of_binders :
-  ?bound:Id.Set.t -> Names.Id.t list -> local_binder list -> Id.Set.t * Names.Id.t list
+  ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
-  glob_constr -> (Names.Id.t * Loc.t) list
+  glob_constr -> (Id.t * Loc.t) list
 
-val make_fresh : Names.Id.Set.t -> Environ.env -> Id.t -> Id.t
+val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Names.Id.Set.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-  Constrexpr.constr_expr * Names.Id.Set.t
+  Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+  Constrexpr.constr_expr * Id.Set.t
 
 val implicit_application : Id.Set.t -> ?allow_partial:bool ->
-  (Names.Id.Set.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-    Constrexpr.constr_expr * Names.Id.Set.t) ->
+  (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+    Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/notation.mli b/interp/notation.mli
index 8b2d8aa0f1..4a28ce2550 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -95,7 +95,7 @@ val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -
 val uninterp_prim_token :
   glob_constr -> scope_name * prim_token
 val uninterp_prim_token_cases_pattern :
-  cases_pattern -> name * scope_name * prim_token
+  cases_pattern -> Name.t * scope_name * prim_token
 val uninterp_prim_token_ind_pattern :
  inductive -> cases_pattern list -> scope_name * prim_token
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a7e5913836..9dcd24127f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -150,14 +150,14 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
-    when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
     on_true_do (f ty1 ty2 & f c1 c2) add na1
   | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
-    when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+    when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
       on_true_do (f ty1 ty2 & f c1 c2) add na1
   | GHole _, GHole _ -> true
   | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2
-  | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when name_eq na1 na2 ->
+  | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
       on_true_do (f b1 b2 & f c1 c2) add na1
   | (GCases _ | GRec _
     | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 35c9a8e1c1..d46657b5c7 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -30,7 +30,7 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->
-  ('a -> name -> 'a * name) ->
+  ('a -> Name.t -> 'a * Name.t) ->
   ('a -> notation_constr -> glob_constr) ->
   'a -> notation_constr -> glob_constr
 
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 3054808400..de72a410d1 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -14,4 +14,4 @@ open Notation_term
 
 val declare_reserved_type : Id.t located list -> notation_constr -> unit
 val find_reserved_type : Id.t -> notation_constr
-val anonymize_if_reserved : name -> glob_constr -> glob_constr
+val anonymize_if_reserved : Name.t -> glob_constr -> glob_constr