Modulification of identifier

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

3 files changed, 10 insertions, 10 deletions

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5b57a0d17..92135d497 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -22,10 +22,10 @@ let string_of_global r =
   let prefix = match Names.repr_dirpath dp with
     | [] -> ""
     | m::_ ->
-      let s = Names.string_of_id m in
+      let s = Names.Id.to_string m in
       if List.mem s meaningful_submodule then s^"." else ""
   in
-  prefix^(Names.string_of_id (Nametab.basename_of_global r))
+  prefix^(Names.Id.to_string (Nametab.basename_of_global r))
 
 let destructurate t =
   let c, args = Term.decompose_app t in
@@ -36,7 +36,7 @@ let destructurate t =
 	Kapp (string_of_global (Globnames.ConstructRef csp), args)
     | Term.Ind isp, args ->
 	Kapp (string_of_global (Globnames.IndRef isp), args)
-    | Term.Var id,[] -> Kvar(Names.string_of_id id)
+    | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
 	Errors.error "Omega: Not a quantifier-free goal"
@@ -296,13 +296,13 @@ let coq_Zneg = lazy (bin_constant "Zneg")
 let recognize t =
   let rec loop t =
     let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
+    match Names.Id.to_string f,l with
        "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
      | "xO",[t] -> Bigint.mult Bigint.two (loop t)
      | "xH",[] -> Bigint.one
      | _ -> failwith "not a number" in
   let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
+    match Names.Id.to_string f,l with
         "Zpos",[t] -> loop t
       | "Zneg",[t] -> Bigint.neg (loop t)
       | "Z0",[] -> Bigint.zero
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 5a843e2b7..a68196e8c 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -37,6 +37,6 @@ END
 
 TACTIC EXTEND romega'
 | [ "romega" "with" ne_ident_list(l) ] ->
-    [ romega_tactic (List.map Names.string_of_id l) ]
+    [ romega_tactic (List.map Names.Id.to_string l) ]
 | [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ]
 END
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e573f2006..e3674fae0 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -40,7 +40,7 @@ type occ_path = occ_step list
 
 (* chemin identifiant une proposition sous forme du nom de l'hypothèse et
    d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurence = {o_hyp : Names.identifier; o_path : occ_path}
+type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
 
 (* \subsection{refiable formulas} *)
 type oformula =
@@ -137,7 +137,7 @@ type context_content =
 
 (* \section{Specific utility functions to handle base types} *)
 (* Nom arbitraire de l'hypothèse codant la négation du but final *)
-let id_concl = Names.id_of_string "__goal__"
+let id_concl = Names.Id.of_string "__goal__"
 
 (* Initialisation de l'environnement de réification de la tactique *)
 let new_environment () = {
@@ -746,7 +746,7 @@ let reify_gl env gl =
       (i,t) :: lhyps ->
 	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
 	if !debug then begin
-	  Printf.printf "  %s: " (Names.string_of_id i);
+	  Printf.printf "  %s: " (Names.Id.to_string i);
 	  pprint stdout t';
 	  Printf.printf "\n"
 	end;
@@ -840,7 +840,7 @@ let display_systems syst_list =
 	 (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M")
 	    oformula_eq.e_origin.o_path));
     Printf.printf "\n  Origin: %s (negated : %s)\n\n"
-      (Names.string_of_id oformula_eq.e_origin.o_hyp)
+      (Names.Id.to_string oformula_eq.e_origin.o_hyp)
       (if oformula_eq.e_negated then "yes" else "no") in
 
   let display_system syst =