diff options
Diffstat (limited to 'plugins/romega/const_omega.ml')
| -rw-r--r-- | plugins/romega/const_omega.ml | 10 |
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 |