Modulification of identifier

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

8 files changed, 22 insertions, 22 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 1c00e6581b..bbc4a0c5ae 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -56,7 +56,7 @@ let cases_pattern_expr_of_name (loc,na) = match na with
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * identifier option
+  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
   | GramConstrListMark of int * bool
     (* tells action rule to make a list of the n previous parsed items;
        concat with last parsed list if true *)
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 3079ffc28a..827e7c1971 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -27,7 +27,7 @@ open Egramml
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * identifier option
+  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
   | GramConstrListMark of int * bool
     (* tells action rule to make a list of the n previous parsed items;
        concat with last parsed list if true *)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index ae7351a9a4..a248047865 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -31,7 +31,7 @@ let make_generic_action
 type grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal of
-      Loc.t * argument_type * prod_entry_key * identifier option
+      Loc.t * argument_type * prod_entry_key * Id.t option
 
 let make_prod_item = function
   | GramTerminal s -> (gram_token_of_string s, None)
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index d38652c974..442b0138f1 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -14,7 +14,7 @@
 type grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal of Loc.t * Genarg.argument_type *
-      Pcoq.prod_entry_key * Names.identifier option
+      Pcoq.prod_entry_key * Names.Id.t option
 
 val extend_tactic_grammar :
   string -> grammar_prod_item list list -> unit
@@ -29,5 +29,5 @@ val get_extend_vernac_grammars :
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
-  (Loc.t -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) ->
+  (Loc.t -> (Names.Id.t * Tacexpr.raw_generic_argument) list -> 'b) ->
   grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1f7a85c8ee..3f246b48cc 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -21,7 +21,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 
 (* TODO: avoid this redefinition without an extra dep to Notation_ops *)
-let ldots_var = id_of_string ".."
+let ldots_var = Id.of_string ".."
 
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
@@ -88,7 +88,7 @@ let lpar_id_coloneq =
                   (match get_tok (stream_nth 2 strm) with
                     | KEYWORD ":=" ->
                         stream_njunk 3 strm;
-                        Names.id_of_string s
+                        Names.Id.of_string s
 	            | _ -> err ())
               | _ -> err ())
         | _ -> err ())
@@ -102,7 +102,7 @@ let impl_ident_head =
 	      | IDENT ("wf"|"struct"|"measure") -> err ()
 	      | IDENT s ->
 		  stream_njunk 2 strm;
-		  Names.id_of_string s
+		  Names.Id.of_string s
 	      | _ -> err ())
 	| _ -> err ())
 
@@ -114,7 +114,7 @@ let name_colon =
             (match get_tok (stream_nth 1 strm) with
               | KEYWORD ":" ->
                   stream_njunk 2 strm;
-                  Name (Names.id_of_string s)
+                  Name (Names.Id.of_string s)
               | _ -> err ())
 	| KEYWORD "_" ->
           (match get_tok (stream_nth 1 strm) with
@@ -135,7 +135,7 @@ GEXTEND Gram
     [ [ id = Prim.ident -> id
 
       (* This is used in quotations and Syntax *)
-      | id = METAIDENT -> id_of_string id ] ]
+      | id = METAIDENT -> Id.of_string id ] ]
   ;
   Prim.name:
     [ [ "_" -> (!@loc, Anonymous) ] ]
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index e868bc77c5..8e52a3babd 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -39,7 +39,7 @@ GEXTEND Gram
     [ [ s = IDENT -> s ] ]
   ;
   ident:
-    [ [ s = IDENT -> id_of_string s ] ]
+    [ [ s = IDENT -> Id.of_string s ] ]
   ;
   pattern_ident:
     [ [ LEFTQMARK; id = ident -> id ] ]
@@ -54,7 +54,7 @@ GEXTEND Gram
     [ [ id = ident -> (!@loc, id) ] ]
   ;
   field:
-    [ [ s = FIELD -> id_of_string s ] ]
+    [ [ s = FIELD -> Id.of_string s ] ]
   ;
   fields:
     [ [ id = field; (l,id') = fields -> (l@[id],id')
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index e1a43c400f..53ade7c2c3 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -79,7 +79,7 @@ let get_xml_attr s al =
 
 (* Interpreting specific attributes *)
 
-let ident_of_cdata (loc,a) = id_of_string a
+let ident_of_cdata (loc,a) = Id.of_string a
 
 let uri_of_data s =
   let n = String.index s ':' in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e9b504e05d..d1fd1edc78 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -159,25 +159,25 @@ module Prim :
     open Names
     open Libnames
     val preident : string Gram.entry
-    val ident : identifier Gram.entry
+    val ident : Id.t Gram.entry
     val name : name located Gram.entry
-    val identref : identifier located Gram.entry
-    val pattern_ident : identifier Gram.entry
-    val pattern_identref : identifier located Gram.entry
-    val base_ident : identifier Gram.entry
+    val identref : Id.t located Gram.entry
+    val pattern_ident : Id.t Gram.entry
+    val pattern_identref : Id.t located Gram.entry
+    val base_ident : Id.t Gram.entry
     val natural : int Gram.entry
     val bigint : Bigint.bigint Gram.entry
     val integer : int Gram.entry
     val string : string Gram.entry
     val qualid : qualid located Gram.entry
-    val fullyqualid : identifier list located Gram.entry
+    val fullyqualid : Id.t list located Gram.entry
     val reference : reference Gram.entry
     val by_notation : (Loc.t * string * string option) Gram.entry
     val smart_global : reference or_by_notation Gram.entry
     val dirpath : dir_path Gram.entry
     val ne_string : string Gram.entry
     val ne_lstring : string located Gram.entry
-    val var : identifier located Gram.entry
+    val var : Id.t located Gram.entry
   end
 
 module Constr :
@@ -187,7 +187,7 @@ module Constr :
     val lconstr : constr_expr Gram.entry
     val binder_constr : constr_expr Gram.entry
     val operconstr : constr_expr Gram.entry
-    val ident : identifier Gram.entry
+    val ident : Id.t Gram.entry
     val global : reference Gram.entry
     val sort : glob_sort Gram.entry
     val pattern : cases_pattern_expr Gram.entry
@@ -197,7 +197,7 @@ module Constr :
     val binder : local_binder list Gram.entry (* closed_binder or variable *)
     val binders : local_binder list Gram.entry (* list of binder *)
     val open_binders : local_binder list Gram.entry
-    val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
+    val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry
     val typeclass_constraint : (name located * bool * constr_expr) Gram.entry
     val record_declaration : constr_expr Gram.entry
     val appl_arg : (constr_expr * explicitation located option) Gram.entry