From 85ed2504568ee06207546b1ac0660e9c559bca22 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Dec 2013 01:15:54 +0100
Subject: Writing [cut] tactic using the new monad.

---
 plugins/fourier/fourierR.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index d49f225e67..2a5e81ec0d 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -616,7 +616,7 @@ let rec fourier gl=
 					 )
 				]));
                        !tac1]);
-	   tac:=(tclTHENS (cut (get coq_False))
+	   tac:=(tclTHENS (Proofview.V82.of_tactic (cut (get coq_False)))
 				  [tclTHEN (Proofview.V82.of_tactic intro) (Proofview.V82.of_tactic (contradiction None));
 				   !tac])
       |_-> assert false) |_-> assert false
-- 
cgit v1.2.3