From d5fece25d8964d5d9fcd55b66164286aeef5fb9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Aug 2014 20:44:03 +0200
Subject: Reorganization of tactics: - made "apply" tactics of type
 Proofview.tactic, as well as other inner   functions about elim and assert -
 used same hypothesis naming policy for intros and internal_cut (towards a  
 reorganization of intro patterns) - "apply ... in H as pat" now supports any
 kind of introduction   pattern (doc not changed)

---
 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 e22816c136..1835b6cc99 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1283,7 +1283,7 @@ let resolution env full_reified_goal systems_list =
   Tactics.generalize
     (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
   Tactics.change_concl reified >>
-  Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
+  Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>
   (*i Alternatives to the previous line:
@@ -1292,7 +1292,7 @@ let resolution env full_reified_goal systems_list =
    - Skip the conversion check and rely directly on the QED:
       Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
   i*)
-  Tactics.apply (Lazy.force coq_I)
+  Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I))
 
 let total_reflexive_omega_tactic gl =
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
-- 
cgit v1.2.3