From 73cdb000ec07ec484557839c4b94fcf779df2f06 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 13 May 2016 00:16:09 +0200
Subject: Put the "clear" tactic into the monad.

---
 tactics/autorewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/autorewrite.ml')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6d6e51536..9ae0ab90b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -151,7 +151,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
                begin
                 let gl'' =
                   if !to_be_cleared then
-                   tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl
+                   tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl
                   else gl' in
                 id := lastid ;
                 to_be_cleared := true ;
-- 
cgit v1.2.3