5 files changed, 16 insertions, 11 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index fbed1df176..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
@@ -226,7 +229,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> Term.constr
   val parse_term : Term.constr -> parse_term
-  val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+  val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val get_scalar : Term.constr -> Bigint.bigint option
 end
@@ -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 ca23ed6c42..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 *)
 
@@ -113,7 +114,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+    val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val get_scalar : Term.constr -> Bigint.bigint option
   end
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 fdcd622994..1a53862ec4 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,9 +6,9 @@
 
  *************************************************************************)
 
+open API
 open Pp
 open Util
-open Proofview.Notations
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1029,7 +1029,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
   Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
 let total_reflexive_omega_tactic unsafe =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
@@ -1043,4 +1043,5 @@ let total_reflexive_omega_tactic unsafe =
   if !debug then display_systems systems_list;
   resolution unsafe env reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
-  end }
+  end
+
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