From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 21:41:55 +0200
Subject: Put the "generalize" tactic in the monad.

---
 plugins/romega/refl_omega.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 177c870b3c..dca46cbcf7 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1280,8 +1280,8 @@ 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 >>
-- 
cgit v1.2.3