diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/const_omega.ml | 7 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4db4bdc2c..06c80a825 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,6 +7,7 @@ *************************************************************************) open API +open Names let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] @@ -39,7 +40,7 @@ let destructurate t = | Term.Ind (isp,_), args -> Kapp (string_of_global (Globnames.IndRef isp), args) | Term.Var id, [] -> Kvar(Names.Id.to_string id) - | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) + | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body) | _ -> Kufo exception DestConstApp @@ -244,7 +245,7 @@ let minus = lazy (z_constant "Z.sub") let recognize_pos t = let rec loop t = let f,l = dest_const_apply t in - match Names.Id.to_string f,l with + match 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 @@ -255,7 +256,7 @@ let recognize_pos t = let recognize_Z t = try let f,l = dest_const_apply t in - match Names.Id.to_string f,l with + match Id.to_string f,l with | "Zpos",[t] -> recognize_pos t | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t) | "Z0",[] -> Some Bigint.zero diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 30d93654b..53f6f42c8 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -19,7 +19,7 @@ open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (MPfile dp) (Label.make name) in + let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in let tac = Tacenv.interp_ltac kn in Tacinterp.eval_tactic tac |