diff options
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 0504efea57..5b25c003d6 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -160,6 +160,13 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tact success. *) val tclONCE : 'a tactic -> 'a tactic +(* [tclONCE e t] succeeds as [t] if [t] has exactly one + success. Otherwise it fails. It may behave differently than [t] as + there may be extra non-logical effects used to discover that [t] + does not have a second success. Moreover the second success may be + conditional on the error recieved: [e] is used. *) +val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic + (* Focuses a tactic at a range of subgoals, found by their indices. *) val tclFOCUS : int -> int -> 'a tactic -> 'a tactic |