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

---
 plugins/firstorder/rules.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index c05015c538..f19cdd2ccc 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -52,7 +52,7 @@ let basename_of_global=function
   | _->assert false
 
 let clear_global=function
-    VarRef id->clear [id]
+    VarRef id-> Proofview.V82.of_tactic (clear [id])
   | _->tclIDTAC
 
 (* connection rules *)
@@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls));
+		tclTHEN (generalize [term]) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
-- 
cgit v1.2.3