diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.mli | 6 |
2 files changed, 6 insertions, 5 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 |