3 files changed, 15 insertions, 6 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b84cf25405..36511386ac 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1492,7 +1492,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..61efa9f545 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,15 +10,24 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
+open Constrarg
+open Pcoq.Prim
+
+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..177c870b3c 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list =
   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