5 files changed, 11 insertions, 6 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index d97dea0397..06c80a8256 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -6,6 +6,9 @@
 
  *************************************************************************)
 
+open API
+open Names
+
 let module_refl_name = "ReflOmegaCore"
 let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
@@ -37,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
@@ -242,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
@@ -253,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/const_omega.mli b/plugins/romega/const_omega.mli
index a452b1a917..6dc5d9f7e5 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -6,6 +6,7 @@
 
  *************************************************************************)
 
+open API
 
 (** Coq objects used in romega *)
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6479c683b2..53f6f42c8e 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+
 DECLARE PLUGIN "romega_plugin"
 
 open Ltac_plugin
@@ -17,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
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 575634174f..1a53862ec4 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,6 +6,7 @@
 
  *************************************************************************)
 
+open API
 open Pp
 open Util
 open Const_omega
diff --git a/plugins/romega/vo.itarget b/plugins/romega/vo.itarget
deleted file mode 100644
index f7a3c41c78..0000000000
--- a/plugins/romega/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-ReflOmegaCore.vo
-ROmega.vo