Modulification of identifier

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

5 files changed, 19 insertions, 19 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 9c31e2c829..c11ffddbfc 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -121,7 +121,7 @@ let possibly_empty_subentries loc (prods,act) =
   let bind_name p v e = match p with
     | None -> e
     | Some id ->
-        let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in
+        let s = Names.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in
   let rec aux = function
     | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >>
     | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
@@ -130,7 +130,7 @@ let possibly_empty_subentries loc (prods,act) =
         bind_name p <:expr< [] >> (aux tl)
     | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
         (* We check at runtime if extraarg s parses "epsilon" *)
-        let s = match p with None -> "_" | Some id -> Names.string_of_id id in
+        let s = match p with None -> "_" | Some id -> Names.Id.to_string id in
         <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit loc t$ with
           [ None -> raise Exit
           | Some v -> v ] in $aux tl$ >>
@@ -163,7 +163,7 @@ let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
     | GramNonTerminal (_,t,_,Some p) :: tl ->
-	let p = Names.string_of_id p in
+	let p = Names.Id.to_string p in
 	<:expr<
           Pcoq.Gram.action
             (fun $lid:p$ ->
@@ -316,10 +316,10 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let t, g = interp_entry_name false None e "" in
-	GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
+	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let t, g = interp_entry_name false None e sep in
-	GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
+	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
 	    Lexer.add_keyword s;
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index 5d46897c60..130f14717e 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -33,7 +33,7 @@ EXTEND
       | "Type" -> Misctypes.GType None ] ]
   ;
   ident:
-    [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ]
+    [ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ]
   ;
   name:
     [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ]
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 4fe6d6aa11..e879f2fff0 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -25,12 +25,12 @@ let loc = CompatLoc.ghost
 let dloc = <:expr< Loc.ghost >>
 
 let mlexpr_of_ident id =
-  <:expr< Names.id_of_string $str:Names.string_of_id id$ >>
+  <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >>
 
 let mlexpr_of_name = function
   | Names.Anonymous -> <:expr< Names.Anonymous >>
   | Names.Name id ->
-      <:expr< Names.Name (Names.id_of_string $str:Names.string_of_id id$) >>
+      <:expr< Names.Name (Names.Id.of_string $str:Names.Id.to_string id$) >>
 
 let mlexpr_of_dirpath dir =
   let l = Names.repr_dirpath dir in
@@ -139,9 +139,9 @@ let mlexpr_of_binder_kind = function
 	$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
 
 let rec mlexpr_of_constr = function
-  | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
+  | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (Id.to_string id) ->
       let loc = of_coqloc loc in
-      anti loc (string_of_id id)
+      anti loc (Id.to_string id)
   | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >>
   | Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index f74031687c..41cd830b52 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -22,7 +22,7 @@ open Compat
 let rec make_patt = function
   | [] -> <:patt< [] >>
   | GramNonTerminal(loc',_,_,Some p)::l ->
-      let p = Names.string_of_id p in
+      let p = Names.Id.to_string p in
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
@@ -30,7 +30,7 @@ let rec make_when loc = function
   | [] -> <:expr< True >>
   | GramNonTerminal(loc',t,_,Some p)::l ->
       let loc' = of_coqloc loc' in
-      let p = Names.string_of_id p in
+      let p = Names.Id.to_string p in
       let l = make_when loc l in
       let loc = CompatLoc.merge loc' loc in
       let t = mlexpr_of_argtype loc' t in
@@ -41,7 +41,7 @@ let rec make_let e = function
   | [] -> e
   | GramNonTerminal(loc,t,_,Some p)::l ->
       let loc = of_coqloc loc in
-      let p = Names.string_of_id p in
+      let p = Names.Id.to_string p in
       let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
       let e = make_let e l in
       let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
@@ -73,7 +73,7 @@ let rec make_args = function
   | [] -> <:expr< [] >>
   | GramNonTerminal(loc,t,_,Some p)::l ->
       let loc = of_coqloc loc in
-      let p = Names.string_of_id p in
+      let p = Names.Id.to_string p in
       <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >>
   | _::l -> make_args l
 
@@ -200,10 +200,10 @@ EXTEND
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let t, g = interp_entry_name false None e "" in
-        GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let t, g = interp_entry_name false None e sep in
-        GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | s = STRING ->
 	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
         GramTerminal s
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 29a59da79f..9ae529ea08 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -21,7 +21,7 @@ let rec make_let e = function
   | [] -> e
   | GramNonTerminal(loc,t,_,Some p)::l ->
       let loc = of_coqloc loc in
-      let p = Names.string_of_id p in
+      let p = Names.Id.to_string p in
       let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
       let e = make_let e l in
       <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
@@ -93,10 +93,10 @@ EXTEND
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let t, g = interp_entry_name false None e "" in
-        GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let t, g = interp_entry_name false None e sep in
-        GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | s = STRING ->
         GramTerminal s
     ] ]