From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:56:25 +0000 Subject: Modulification of identifier git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/romega/const_omega.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/romega/const_omega.ml') 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 -- cgit v1.2.3