diff options
| author | Jason Gross | 2020-05-02 13:25:43 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-02 13:25:43 -0400 |
| commit | 9b937b6f53c5e97faa5c7949e6032837f8708761 (patch) | |
| tree | a21812c8e0e4af53bab6a71cd68f22b8addbdc4f /engine/proofview.mli | |
| parent | 206e8adedae1b0c479a2cb598510163f909f1a5f (diff) | |
Move tclWRAPFINALLY to profile_ltac
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 70513c8166..d0a2b37a69 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -208,16 +208,6 @@ val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic exception can be assumed non critical. *) val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic -(** [tclWRAPFINALLY before tac finally] runs [before] before each - entry-point of [tac] and passes the result of [before] to - [finally], which is then run at each exit-point of [tac], - regardless of whether it succeeds or fails. Said another way, if - [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun - ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with - [e], it behaves as [before >>= fun v -> finally v <*> tclZERO - e]. *) -val tclWRAPFINALLY : 'a tactic -> 'b tactic -> ('a -> unit tactic) -> 'b tactic - (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails with [e], [tclONCE t] also fails with [e]. *) |