From bda7852cb0896727389935f420eec0e8e3315cf7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Jun 2014 15:04:06 +0200
Subject: Passing some tactics to the new monad type.

---
 plugins/decl_mode/decl_proof_instr.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97989e2687..c230a98963 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -437,7 +437,7 @@ let thus_tac c ctyp submetas gls =
     with Not_found ->
       error "I could not relate this statement to the thesis." in
   if List.is_empty list then
-    exact_check proof gls
+    Proofview.V82.of_tactic (exact_check proof) gls
   else
     let refiner = concl_refiner list proof gls in
       Tactics.refine refiner gls
@@ -534,14 +534,14 @@ let instr_rew _thus rew_side cut gls0 =
 	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
 	      [tclTHEN tcl_erase_info
 		 (tclTHENS (Proofview.V82.of_tactic (transitivity lhs))
-		    [just_tac;exact_check (mkVar last_id)]);
+		    [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]);
 	       thus_tac new_eq] gls0
       | Rhs ->
 	  let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
 	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
 	      [tclTHEN tcl_erase_info
 		 (tclTHENS (Proofview.V82.of_tactic (transitivity rhs))
-		    [exact_check (mkVar last_id);just_tac]);
+		    [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]);
 	       thus_tac new_eq] gls0
 
 
-- 
cgit v1.2.3