diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-28 15:14:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-28 22:45:24 +0200 |
| commit | 58543b45425b85233c068f9da859996270d1fdcf (patch) | |
| tree | 6981dca5a3bf4468d2533bb239dcf44aca190ebf | |
| parent | 32c83676c96ae4a218de0bec75d2f3353381dfb3 (diff) | |
Simplification of the tclCHECKINTERRUPT tactic.
| -rw-r--r-- | proofs/proofview.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.mli | 6 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
3 files changed, 7 insertions, 6 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a75059891..388c60c3f 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 b10cc1843..b1466fcfb 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 bbd114c28..50f51de21 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 = |