4 files changed, 21 insertions, 11 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b84cf25405..5e43dfc42d 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1074,16 +1074,19 @@ Qed.
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_beq t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_bgt t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
@@ -1492,7 +1495,7 @@ with Simplify := match goal with
   end.
 
 Ltac prove_stable x th :=
-  match constr:x with
+  match constr:(x) with
   | ?X1 =>
       unfold term_stable, X1; intros; Simplify; simpl;
        apply th
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 0a99a26b36..fd4ede6c3d 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,15 +10,23 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
+open Constrarg
+
+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 tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
 
 let romega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 560e6a899e..a059512d84 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -9,7 +9,7 @@
 open Pp
 open Util
 open Const_omega
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
 (* \section{Useful functions and flags} *)
@@ -172,7 +172,7 @@ let print_env_reification env =
   in
   let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
   let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in
-  msg_debug (prop_info ++ fnl () ++ term_info)
+  Feedback.msg_debug (prop_info ++ fnl () ++ term_info)
 
 (* \subsection{Gestion des environnements de variable pour Omega} *)
 (* generation d'identifiant d'equation pour Omega *)
@@ -1280,12 +1280,12 @@ let resolution env full_reified_goal systems_list =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Tactics.generalize
-    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
+  Proofview.V82.of_tactic (Tactics.generalize
+    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
   Proofview.V82.of_tactic (Tactics.change_concl reified) >>
   Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
-  Tactics.normalise_vm_in_concl >>
+  Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
   (*i Alternatives to the previous line:
    - Normalisation without VM:
       Tactics.normalise_in_concl
diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mlpack
index 1625009d06..38d0e94111 100644
--- a/plugins/romega/romega_plugin.mllib
+++ b/plugins/romega/romega_plugin.mlpack
@@ -1,4 +1,3 @@
 Const_omega
 Refl_omega
 G_romega
-Romega_plugin_mod