2 files changed, 8 insertions, 7 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index ad3afafd85..949cba2dbe 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -69,19 +69,19 @@ let z_module = [["Coq";"ZArith";"BinInt"]]
 
 let init_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x
 let constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" coq_modules x
 let z_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" z_module x
 let bin_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" bin_module x
 
 (* Logic *)
@@ -170,7 +170,7 @@ let mk_list univ typ l =
   loop l
 
 let mk_plist =
-  let type1lev = Universes.new_univ_level () in
+  let type1lev = UnivGen.new_univ_level () in
   fun l -> mk_list type1lev EConstr.mkProp l
 
 let mk_list = mk_list Univ.Level.set
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index d182497840..e603480656 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Util
+open Constr
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1036,13 +1037,13 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
   let decompose_tactic = decompose_tree env context solution_tree in
 
   Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >>
-  Tactics.convert_concl_no_check reified Term.DEFAULTcast >>
+  Tactics.convert_concl_no_check reified DEFAULTcast >>
   Tactics.apply (app coq_do_omega [|decompose_tactic|]) >>
   show_goal >>
   (if unsafe then
      (* Trust the produced term. Faster, but might fail later at Qed.
         Also handy when debugging, e.g. via a Show Proof after romega. *)
-     Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast
+     Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast
    else
      Tactics.normalise_vm_in_concl) >>
   Tactics.apply (Lazy.force coq_I)