diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-01-31 15:04:44 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-01-31 18:30:00 +0100 |
| commit | 07d63bf9af363e4924ca14cb88b723c8ed2ea2dc (patch) | |
| tree | 0d8c4fcbbdeb68603f385203a579a31fcf39098c /proofs | |
| parent | c734ccd8081e52ee5576d0efac9b065d4f37f7d5 (diff) | |
Typos in comment.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2f215ba94..fed7c1dfd 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -168,11 +168,11 @@ 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 +(* [tclEXACTLY_ONCE 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. *) + conditional on the error received: [e] is used. *) val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic (* Focuses a tactic at a range of subgoals, found by their indices. |