diff options
| author | Pierre-Marie Pédrot | 2014-07-06 17:08:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-08 00:06:02 +0200 |
| commit | eb7753109a849aaa7fe5c341f02e408c5fc49f85 (patch) | |
| tree | 8a9db87dd947e85b9fb317fe11175f45e0229b8e /proofs/proofview.mli | |
| parent | a3503c0aca07f5e7f5785faa7b76123a02ecc2af (diff) | |
Exporting Proof.split in proofview.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6a2d815114..affe276800 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -124,6 +124,10 @@ val unfocus : focus_context -> proofview -> proofview type +'a tactic +type 'a case = +| Fail of exn +| Next of 'a * (exn -> 'a tactic) + (* Applies a tactic to the current proofview. *) (* the return boolean signals the use of an unsafe tactic, in which case it is [false]. *) @@ -160,6 +164,9 @@ val tclZERO : exn -> 'a tactic or [t2 e] if [t1] fails with [e]. *) val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic +(* [tclCASE t] observes the head of the tactic and returns it as a value *) +val tclCASE : 'a tactic -> 'a case tactic + (* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a] fails with [e], then it behaves as [f e]. *) |