Modulification of name

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

7 files changed, 34 insertions, 34 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index a67e591853..68a65c5c70 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -67,16 +67,16 @@ type constr_expr =
   | CCoFix of Loc.t * Id.t located * cofix_expr list
   | CProdN of Loc.t * binder_expr list * constr_expr
   | CLambdaN of Loc.t * binder_expr list * constr_expr
-  | CLetIn of Loc.t * name located * constr_expr * constr_expr
+  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
   | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list
   | CApp of Loc.t * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
   | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
   | CCases of Loc.t * case_style * constr_expr option *
       case_expr list * branch_expr list
-  | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) *
+  | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) *
       constr_expr * constr_expr
-  | CIf of Loc.t * constr_expr * (name located option * constr_expr option)
+  | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of Loc.t * Evar_kinds.t option
   | CPatVar of Loc.t * (bool * patvar)
@@ -89,13 +89,13 @@ type constr_expr =
   | CDelimiters of Loc.t * string * constr_expr
 
 and case_expr =
-  constr_expr * (name located option * cases_pattern_expr option)
+  constr_expr * (Name.t located option * cases_pattern_expr option)
 
 and branch_expr =
   Loc.t * cases_pattern_expr list located list * constr_expr
 
 and binder_expr =
-  name located list * binder_kind * constr_expr
+  Name.t located list * binder_kind * constr_expr
 
 and fix_expr =
     Id.t located * (Id.t located option * recursion_order_expr) *
@@ -111,15 +111,15 @@ and recursion_order_expr =
 
 (** Anonymous defs allowed ?? *)
 and local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * binder_kind * constr_expr
+  | LocalRawDef of Name.t located * constr_expr
+  | LocalRawAssum of Name.t located list * binder_kind * constr_expr
 
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
     constr_expr list list * (** for recursive notations *)
     local_binder list list (** for binders subexpressions *)
 
-type typeclass_constraint = name located * binding_kind * constr_expr
+type typeclass_constraint = Name.t located * binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 596f6b889a..1541d4e46f 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -19,7 +19,7 @@ type obligation_definition_status = Define of bool | Expand
 type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
-  | BinderType of name
+  | BinderType of Name.t
   | QuestionMark of obligation_definition_status
   | CasesType
   | InternalHole
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b8d6564a64..315b11517d 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -23,8 +23,8 @@ open Misctypes
 
      locs here refers to the ident's location, not whole pat *)
 type cases_pattern =
-  | PatVar of Loc.t * name
-  | PatCstr of Loc.t * constructor * cases_pattern list * name
+  | PatVar of Loc.t * Name.t
+  | PatCstr of Loc.t * constructor * cases_pattern list * Name.t
       (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
 
 type glob_constr =
@@ -33,23 +33,23 @@ type glob_constr =
   | GEvar of Loc.t * existential_key * glob_constr list option
   | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
   | GApp of Loc.t * glob_constr * glob_constr list
-  | GLambda of Loc.t * name * binding_kind *  glob_constr * glob_constr
-  | GProd of Loc.t * name * binding_kind * glob_constr * glob_constr
-  | GLetIn of Loc.t * name * glob_constr * glob_constr
+  | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
+  | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
 	  [MatchStyle]) *)
 
-  | GLetTuple of Loc.t * name list * (name * glob_constr option) *
+  | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
       glob_constr * glob_constr
-  | GIf of Loc.t * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
+  | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr
   | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array *
       glob_constr array * glob_constr array
   | GSort of Loc.t * glob_sort
   | GHole of (Loc.t * Evar_kinds.t)
   | GCast of Loc.t * glob_constr * glob_constr cast_type
 
-and glob_decl = name * binding_kind * glob_constr option * glob_constr
+and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr
 
 and fix_recursion_order =
   | GStructRec
@@ -61,7 +61,7 @@ and fix_kind =
   | GCoFix of int
 
 and predicate_pattern =
-    name * (Loc.t * inductive * name list) option
+    Name.t * (Loc.t * inductive * Name.t list) option
       (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
 
 and tomatch_tuple = (glob_constr * predicate_pattern)
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 2b1286940f..411b14f1f1 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -27,19 +27,19 @@ type notation_constr =
   | NHole of Evar_kinds.t
   | NList of Id.t * Id.t * notation_constr * notation_constr * bool
   (** Part only in [glob_constr] *)
-  | NLambda of name * notation_constr * notation_constr
-  | NProd of name * notation_constr * notation_constr
+  | NLambda of Name.t * notation_constr * notation_constr
+  | NProd of Name.t * notation_constr * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr
-  | NLetIn of name * notation_constr * notation_constr
+  | NLetIn of Name.t * notation_constr * notation_constr
   | NCases of case_style * notation_constr option *
-      (notation_constr * (name * (inductive * name list) option)) list *
+      (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
       (cases_pattern list * notation_constr) list
-  | NLetTuple of name list * (name * notation_constr option) *
+  | NLetTuple of Name.t list * (Name.t * notation_constr option) *
       notation_constr * notation_constr
-  | NIf of notation_constr * (name * notation_constr option) *
+  | NIf of notation_constr * (Name.t * notation_constr option) *
       notation_constr * notation_constr
   | NRec of fix_kind * Id.t array *
-      (name * notation_constr option * notation_constr) list array *
+      (Name.t * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort
   | NPatVar of patvar
diff --git a/intf/pattern.mli b/intf/pattern.mli
index 5c0dfbd5da..cec3fe87d1 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -65,9 +65,9 @@ type constr_pattern =
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
-  | PLambda of name * constr_pattern * constr_pattern
-  | PProd of name * constr_pattern * constr_pattern
-  | PLetIn of name * constr_pattern * constr_pattern
+  | PLambda of Name.t * constr_pattern * constr_pattern
+  | PProd of Name.t * constr_pattern * constr_pattern
+  | PLetIn of Name.t * constr_pattern * constr_pattern
   | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 08063cf2ae..1d7e9374f5 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -79,8 +79,8 @@ type 'a match_pattern =
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
-  | Hyp of name located * 'a match_pattern
-  | Def of name located * 'a match_pattern * 'a match_pattern
+  | Hyp of Name.t located * 'a match_pattern
+  | Def of Name.t located * 'a match_pattern * 'a match_pattern
 
 (* Type of a Match rule for Match Context and Match *)
 type ('a,'t) match_rule =
@@ -112,9 +112,9 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacAssert of
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
       intro_pattern_expr located option * 'trm
-  | TacGeneralize of ('trm with_occurrences * name) list
+  | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacGeneralizeDep of 'trm
-  | TacLetTac of name * 'trm * 'nam clause_expr * letin_flag *
+  | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
       intro_pattern_expr located option
 
   (* Derived basic tactics *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 8088ba92a9..52120d73c3 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -19,7 +19,7 @@ open Libnames
 (** Vernac expressions, produced by the parser *)
 
 type lident = Id.t located
-type lname = name located
+type lname = Name.t located
 type lstring = string located
 type lreference = reference
 
@@ -317,7 +317,7 @@ type vernac_expr =
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
       (explicitation * bool * bool) list list
   | VernacArguments of locality_flag * reference or_by_notation *
-      ((name * bool * (Loc.t * string) option * bool * bool) list) list *
+      ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list *
       int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
   | VernacArgumentsScope of locality_flag * reference or_by_notation *