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/rtauto/refl_tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index bff574a062..6b4be4e2aa 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -313,7 +313,7 @@ let rtauto_tac gls=
   let tac_start_time = System.get_time () in
   let result=
     if !check then
-      Tactics.exact_check term gls
+      Proofview.V82.of_tactic (Tactics.exact_check term) gls
     else
       Tactics.exact_no_check term gls in
   let tac_end_time = System.get_time () in
-- 
cgit v1.2.3