Modulification of identifier

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

10 files changed, 52 insertions, 52 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 01380b8d5a..a67e591853 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -19,8 +19,8 @@ open Decl_kinds
 type notation = string
 
 type explicitation =
-  | ExplByPos of int * identifier option
-  | ExplByName of identifier
+  | ExplByPos of int * Id.t option
+  | ExplByName of Id.t
 
 type binder_kind =
   | Default of binding_kind
@@ -35,15 +35,15 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 type prim_token = Numeral of Bigint.bigint | String of string
 
 type raw_cases_pattern_expr =
-  | RCPatAlias of Loc.t * raw_cases_pattern_expr * identifier
+  | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
   | RCPatCstr of Loc.t * Globnames.global_reference
     * raw_cases_pattern_expr list * raw_cases_pattern_expr list
   (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
-  | RCPatAtom of Loc.t * identifier option
+  | RCPatAtom of Loc.t * Id.t option
   | RCPatOr of Loc.t * raw_cases_pattern_expr list
 
 type cases_pattern_expr =
-  | CPatAlias of Loc.t * cases_pattern_expr * identifier
+  | CPatAlias of Loc.t * cases_pattern_expr * Id.t
   | CPatCstr of Loc.t * reference
     * cases_pattern_expr list * cases_pattern_expr list
   (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
@@ -63,8 +63,8 @@ and cases_pattern_notation_substitution =
 
 type constr_expr =
   | CRef of reference
-  | CFix of Loc.t * identifier located * fix_expr list
-  | CCoFix of Loc.t * identifier located * cofix_expr list
+  | CFix of Loc.t * Id.t located * fix_expr list
+  | 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
@@ -98,11 +98,11 @@ and binder_expr =
   name located list * binder_kind * constr_expr
 
 and fix_expr =
-    identifier located * (identifier located option * recursion_order_expr) *
+    Id.t located * (Id.t located option * recursion_order_expr) *
       local_binder list * constr_expr * constr_expr
 
 and cofix_expr =
-    identifier located * local_binder list * constr_expr * constr_expr
+    Id.t located * local_binder list * constr_expr * constr_expr
 
 and recursion_order_expr =
   | CStructRec
@@ -128,8 +128,8 @@ type constr_pattern_expr = constr_expr
 (** Concrete syntax for modules and module types *)
 
 type with_declaration_ast =
-  | CWith_Module of identifier list located * qualid located
-  | CWith_Definition of identifier list located * constr_expr
+  | CWith_Module of Id.t list located * qualid located
+  | CWith_Definition of Id.t list located * constr_expr
 
 type module_ast =
   | CMident of qualid located
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 90ada0e3df..596f6b889a 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -17,7 +17,7 @@ open Globnames
 type obligation_definition_status = Define of bool | Expand
 
 type t =
-  | ImplicitArg of global_reference * (int * identifier option)
+  | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of name
   | QuestionMark of obligation_definition_status
@@ -26,4 +26,4 @@ type t =
   | TomatchTypeParameter of inductive * int
   | GoalEvar
   | ImpossibleCase
-  | MatchingVar of bool * identifier
+  | MatchingVar of bool * Id.t
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 63d945b7c7..833d32545d 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -44,5 +44,5 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (Loc.t * Names.identifier) * 'a
+  | ConstrContext of (Loc.t * Names.Id.t) * 'a
   | ConstrTypeOf of 'a
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 8e7b012b0a..b8d6564a64 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -29,7 +29,7 @@ type cases_pattern =
 
 type glob_constr =
   | GRef of (Loc.t * global_reference)
-  | GVar of (Loc.t * identifier)
+  | GVar of (Loc.t * Id.t)
   | 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
@@ -43,7 +43,7 @@ type glob_constr =
   | GLetTuple of Loc.t * name list * (name * glob_constr option) *
       glob_constr * glob_constr
   | GIf of Loc.t * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
-  | GRec of Loc.t * fix_kind * identifier array * glob_decl list array *
+  | 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)
@@ -68,7 +68,7 @@ and tomatch_tuple = (glob_constr * predicate_pattern)
 
 and tomatch_tuples = tomatch_tuple list
 
-and cases_clause = (Loc.t * identifier list * cases_pattern list * glob_constr)
+and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr)
 (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
     of [t] are members of [il]. *)
 and cases_clauses = cases_clause list
diff --git a/intf/locus.mli b/intf/locus.mli
index 9073b6ae86..e0ce43331e 100644
--- a/intf/locus.mli
+++ b/intf/locus.mli
@@ -49,7 +49,7 @@ type 'id clause_expr =
   { onhyps : 'id hyp_location_expr list option;
     concl_occs : occurrences_expr }
 
-type clause = identifier clause_expr
+type clause = Id.t clause_expr
 
 
 (** {6 Concrete view of occurrence clauses} *)
@@ -59,7 +59,7 @@ type clause = identifier clause_expr
    or in both) or to some occurrences of the conclusion *)
 
 type clause_atom =
-  | OnHyp of identifier * occurrences_expr * hyp_location_flag
+  | OnHyp of Id.t * occurrences_expr * hyp_location_flag
   | OnConcl of occurrences_expr
 
 (** A [concrete_clause] is an effective collection of occurrences
@@ -72,7 +72,7 @@ type concrete_clause = clause_atom list
 
 (** A [hyp_location] is an hypothesis together with a location *)
 
-type hyp_location = identifier * hyp_location_flag
+type hyp_location = Id.t * hyp_location_flag
 
 (** A [goal_location] is either an hypothesis (together with a location)
     or the conclusion (represented by None) *)
@@ -85,4 +85,4 @@ type goal_location = hyp_location option
 (** A [simple_clause] is a set of hypotheses, possibly extended with
    the conclusion (conclusion is represented by None) *)
 
-type simple_clause = identifier option list
+type simple_clause = Id.t option list
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index f46ada4457..3a044018c4 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -12,7 +12,7 @@ open Names
 
 (** Cases pattern variables *)
 
-type patvar = identifier
+type patvar = Id.t
 
 (** Introduction patterns *)
 
@@ -20,8 +20,8 @@ type intro_pattern_expr =
   | IntroOrAndPattern of or_and_intro_pattern_expr
   | IntroWildcard
   | IntroRewrite of bool
-  | IntroIdentifier of identifier
-  | IntroFresh of identifier
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
   | IntroForthcoming of bool
   | IntroAnonymous
 and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list
@@ -61,7 +61,7 @@ type 'a cast_type =
 
 (** Bindings *)
 
-type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
+type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
 
 type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list
 
@@ -77,9 +77,9 @@ type 'a with_bindings = 'a * 'a bindings
 
 type 'a or_var =
   | ArgArg of 'a
-  | ArgVar of Names.identifier Loc.located
+  | ArgVar of Names.Id.t Loc.located
 
-type 'a and_short_name = 'a * identifier Loc.located option
+type 'a and_short_name = 'a * Id.t Loc.located option
 
 type 'a or_by_notation =
   | AN of 'a
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index d7bd73588e..2b1286940f 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -22,14 +22,14 @@ open Glob_term
 type notation_constr =
   (** Part common to [glob_constr] and [cases_pattern] *)
   | NRef of global_reference
-  | NVar of identifier
+  | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t
-  | NList of identifier * identifier * notation_constr * notation_constr * bool
+  | 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
-  | NBinderList of identifier * identifier * notation_constr * notation_constr
+  | NBinderList of Id.t * Id.t * notation_constr * notation_constr
   | NLetIn of name * notation_constr * notation_constr
   | NCases of case_style * notation_constr option *
       (notation_constr * (name * (inductive * name list) option)) list *
@@ -38,7 +38,7 @@ type notation_constr =
       notation_constr * notation_constr
   | NIf of notation_constr * (name * notation_constr option) *
       notation_constr * notation_constr
-  | NRec of fix_kind * identifier array *
+  | NRec of fix_kind * Id.t array *
       (name * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort
@@ -71,5 +71,5 @@ type notation_var_internalization_type =
 
 (** This characterizes to what a notation is interpreted to *)
 type interpretation =
-    (identifier * (subscopes * notation_var_instance_type)) list *
+    (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
diff --git a/intf/pattern.mli b/intf/pattern.mli
index a8c787673d..5c0dfbd5da 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -43,7 +43,7 @@ open Misctypes
     could be inferred. We also loose the ability of typing ltac
     variables before calling the right-hand-side of ltac matching clauses. *)
 
-type constr_under_binders = identifier list * constr
+type constr_under_binders = Id.t list * constr
 
 (** Types of substitutions with or w/o bound variables *)
 
@@ -60,7 +60,7 @@ type case_info_pattern =
 
 type constr_pattern =
   | PRef of global_reference
-  | PVar of identifier
+  | PVar of Id.t
   | PEvar of existential_key * constr_pattern array
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 1f1388e3db..26ab4b6667 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -34,7 +34,7 @@ type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
-  | ElimOnIdent of identifier located
+  | ElimOnIdent of Id.t located
   | ElimOnAnonHyp of int
 
 type inversion_kind =
@@ -75,7 +75,7 @@ type multi =
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
-  | Subterm of bool * identifier option * 'a
+  | Subterm of bool * Id.t option * 'a
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
@@ -93,7 +93,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of intro_pattern_expr located list
   | TacIntrosUntil of quantified_hypothesis
-  | TacIntroMove of identifier option * 'nam move_location
+  | TacIntroMove of Id.t option * 'nam move_location
   | TacAssumption
   | TacExact of 'trm
   | TacExactNoCheck of 'trm
@@ -104,10 +104,10 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacElimType of 'trm
   | TacCase of evars_flag * 'trm with_bindings
   | TacCaseType of 'trm
-  | TacFix of identifier option * int
-  | TacMutualFix of identifier * int * (identifier * int * 'trm) list
-  | TacCofix of identifier option
-  | TacMutualCofix of identifier * (identifier * 'trm) list
+  | TacFix of Id.t option * int
+  | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
+  | TacCofix of Id.t option
+  | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacCut of 'trm
   | TacAssert of
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
@@ -167,7 +167,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
 
   (* For syntax extensions *)
   | TacAlias of Loc.t * string *
-      (identifier * 'lev generic_argument) list * (dir_path * glob_tactic_expr)
+      (Id.t * 'lev generic_argument) list * (dir_path * glob_tactic_expr)
 
 (** Possible arguments of a tactic definition *)
 
@@ -213,12 +213,12 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacProgress of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacShowHyps of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacAbstract of
-      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * identifier option
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * Id.t option
   | TacId of 'n message_token list
   | TacFail of int or_var * 'n message_token list
   | TacInfo of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacLetIn of rec_flag *
-      (identifier located * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg) list *
+      (Id.t located * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg) list *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacMatch of lazy_flag *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
@@ -229,7 +229,7 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacArg of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg located
 
 and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
-    identifier option list * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+    Id.t option list * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
 
 (** Globalized tactics *)
 
@@ -238,7 +238,7 @@ and g_pat = glob_constr_and_expr * constr_pattern
 and g_cst = evaluable_global_reference and_short_name or_var
 and g_ind = inductive or_var
 and g_ref = ltac_constant located or_var
-and g_nam  = identifier located
+and g_nam  = Id.t located
 
 and glob_tactic_expr =
     (g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr
@@ -256,7 +256,7 @@ type r_pat = constr_pattern_expr
 type r_cst = reference or_by_notation
 type r_ind = reference or_by_notation
 type r_ref = reference
-type r_nam  = identifier located or_metaid
+type r_nam  = Id.t located or_metaid
 type r_lev = rlevel
 
 type raw_atomic_tactic_expr =
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f1eebc18e6..16175be0d0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -18,7 +18,7 @@ open Libnames
 
 (** Vernac expressions, produced by the parser *)
 
-type lident = identifier located
+type lident = Id.t located
 type lname = name located
 type lstring = string located
 type lreference = reference
@@ -151,10 +151,10 @@ type definition_expr =
       * constr_expr option
 
 type fixpoint_expr =
-    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+    Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
-    identifier located * local_binder list * constr_expr * constr_expr option
+    Id.t located * local_binder list * constr_expr * constr_expr option
 
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
@@ -184,7 +184,7 @@ type module_binder = bool option * lident list * module_ast_inl
 
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
-  | TacNonTerm of Loc.t * string * (Names.identifier * string) option
+  | TacNonTerm of Loc.t * string * (Names.Id.t * string) option
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
@@ -312,7 +312,7 @@ type vernac_expr =
   | VernacCreateHintDb of locality_flag * string * bool
   | VernacRemoveHints of locality_flag * string list * reference list
   | VernacHints of locality_flag * string list * hints_expr
-  | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
+  | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
       (explicitation * bool * bool) list list