diff options
| author | Pierre-Marie Pédrot | 2014-07-24 15:11:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-24 15:13:12 +0200 |
| commit | ae5ea0c9d5c0e9a39a50a2348b2b8f08938d5f5c (patch) | |
| tree | 2ba9b3c26e3627fe70bf095bdf650c8d375e9176 /proofs/proofview.ml | |
| parent | fb4187a6d475719bada0a7fe1b7902a36e06d658 (diff) | |
Adding a tail-rec tclONCE.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 1797f38f0f..52d8b7d7ca 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -283,12 +283,7 @@ let tclIFCATCH a s f = (* [tclONCE t] fails if [t] fails, otherwise it has exactly one success. *) -let tclONCE t = - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Proof.bind in - Proof.split t >>= function - | Nil e -> tclZERO e - | Cons (x,_) -> tclUNIT x +let tclONCE = Proof.once exception MoreThanOneSuccess let _ = Errors.register_handler begin function |