From 58543b45425b85233c068f9da859996270d1fdcf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 28 Aug 2014 15:14:29 +0200
Subject: Simplification of the tclCHECKINTERRUPT tactic.

---
 proofs/proofview.ml  | 5 +++--
 proofs/proofview.mli | 6 +++---
 tactics/tacticals.ml | 2 +-
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a750598912..388c60c3f5 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -231,8 +231,6 @@ let catchable_exception = function
 (* Unit of the tactic monad *)
 let tclUNIT a = (Proof.ret a:'a Proof.t)
 
-let tclCHECKINTERRUPT a = Control.check_for_interrupt (); Proof.ret a
-
 (* Bind operation of the tactic monad *)
 let tclBIND = Proof.bind
 
@@ -988,3 +986,6 @@ end
 module NonLogical = Proofview_monad.NonLogical
 
 let tclLIFT = Proofview_monad.Logical.lift
+
+let tclCHECKINTERRUPT =
+  tclLIFT (NonLogical.make Control.check_for_interrupt)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b10cc18433..b1466fcfb5 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -140,9 +140,6 @@ val apply : Environ.env -> 'a tactic -> proofview -> 'a
 (* Unit of the tactic monad *)
 val tclUNIT : 'a -> 'a tactic
  
-(* Unit but checks for interrupts *) 
-val tclCHECKINTERRUPT : 'a -> 'a tactic
-
 (* Bind operation of the tactic monad *)
 val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
 
@@ -259,6 +256,9 @@ val tclIN_ENV : Environ.env -> 'a tactic -> 'a tactic
 (* [tclEFFECTS eff] add the effects [eff] to the current state. *)
 val tclEFFECTS : Declareops.side_effects -> unit tactic
 
+(* Checks for interrupts *)
+val tclCHECKINTERRUPT : unit tactic
+
 (* Shelves all the goals under focus. The goals are placed on the
    shelf for later use (or being solved by side-effects). *)
 val shelve : unit tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bbd114c281..50f51de21c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -411,7 +411,7 @@ module New = struct
   let rec tclREPEAT0 t =
     tclINDEPENDENT begin
       tclIFCATCH t
-        (fun () -> tclCHECKINTERRUPT () <*> tclREPEAT0 t)
+        (fun () -> tclCHECKINTERRUPT <*> tclREPEAT0 t)
         (fun e -> catch_failerror e <*> tclUNIT ())
     end
   let tclREPEAT t =
-- 
cgit v1.2.3