Modulification of identifier

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

1 files changed, 5 insertions, 5 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