3 files changed, 24 insertions, 11 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index ad3afafd..949cba2d 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/g_romega.ml4 b/plugins/romega/g_romega.mlg
index 5b77d08d..ac4f30b1 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.mlg
@@ -9,6 +9,8 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+{
+
 open Ltac_plugin
 open Names
 open Refl_omega
@@ -39,13 +41,23 @@ let romega_tactic unsafe l =
        (Tactics.intros)
        (total_reflexive_omega_tactic unsafe))
 
+let romega_depr =
+  Vernacinterp.mk_deprecation
+    ~since:(Some "8.9")
+    ~note:(Some "Use lia instead.")
+    ()
+
+}
+
 TACTIC EXTEND romega
-|  [ "romega" ] -> [ romega_tactic false [] ]
-|  [ "unsafe_romega" ] -> [ romega_tactic true [] ]
+DEPRECATED { romega_depr }
+|  [ "romega" ] -> { romega_tactic false [] }
+|  [ "unsafe_romega" ] -> { romega_tactic true [] }
 END
 
 TACTIC EXTEND romega'
+DEPRECATED { romega_depr }
 | [ "romega" "with" ne_ident_list(l) ] ->
-    [ romega_tactic false (List.map Names.Id.to_string l) ]
-| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ]
+    { romega_tactic false (List.map Names.Id.to_string l) }
+| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
 END
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index d1824978..e6034806 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)