2 files changed, 29 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 823082aced..bb1d5758d6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -253,6 +253,28 @@ let tclONCE t =
     | Nil e -> tclZERO e
     | Cons (x,_) -> tclUNIT x
 
+exception MoreThanOneSuccess
+let _ = Errors.register_handler begin function
+  | MoreThanOneSuccess -> Errors.error "This tactic has more than one success."
+  | _ -> raise Errors.Unhandled
+end
+
+(* [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. *)
+let tclEXACTLY_ONCE e t =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.split t >>= function
+    | Nil e -> tclZERO e
+    | Cons (x,k) ->
+        Proof.split (k e) >>= function
+          | Nil _ -> tclUNIT x
+          | _ -> tclZERO MoreThanOneSuccess
+
+
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 (* arnaud: bug if 0 goals ! *)
 let tclFOCUS i j t =
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