Specializing tclBREAK so that it can choose the return exception in case

of a break.

4 files changed, 11 insertions, 16 deletions

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 9ac7faaf2..ac9fea772 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -262,10 +262,10 @@ struct
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
 
-  let break (f : exn -> bool) (m : 'a t) : 'a t = (); fun s ->
+  let break (f : exn -> exn option) (m : 'a t) : 'a t = (); fun s ->
     let m = m s in
     { iolist = fun nil cons ->
-      m.iolist nil (fun x next -> cons x (fun e -> if f e then nil e else next e))
+      m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e))
     }
 
   (** For [reflect] and [split] see the "Backtracking, Interleaving,
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index c1315e9f5..3d6866514 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -136,7 +136,7 @@ module Logical (P:Param) : sig
   val plus : 'a t -> (exn -> 'a t) -> 'a t
   val split : 'a t -> (('a,(exn->'a t)) list_view) t
   val once : 'a t -> 'a t
-  val break : (exn -> bool) -> 'a t -> 'a t
+  val break : (exn -> exn option) -> 'a t -> 'a t
 
   val lift : 'a NonLogical.t -> 'a t
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 3529c3c1b..293d99fdc 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -213,10 +213,10 @@ val tclCASE : 'a tactic -> 'a case tactic
 
 (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
     stopping after the first success, it succeeds like [t] until a
-    failure with an exception [e] such that [p e=true] is raised. At
-    which point it drop the remaining successes. [tclONCE t] is
-    equivalent to [tclBREAK (fun _ -> true) t]. *)
-val tclBREAK : (exn -> bool) -> 'a tactic -> 'a tactic
+    failure with an exception [e] such that [p e = Some e'] is raised. At
+    which point it drops the remaining successes, failing with [e'].
+    [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
+val tclBREAK : (exn -> exn option) -> 'a tactic -> 'a tactic
 
 
 (** {7 Focusing tactics} *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 443ec5aae..2055bd7ea 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1472,19 +1472,14 @@ and interp_match_successes lz ist tac =
       let tac = Proofview.tclONCE tac in
       tac >>= fun ans -> interp_match_success ist ans
     else
-      let decrease e = match e with
-      | FailError (0, _) -> e
-      | FailError (n, s) -> FailError (pred n, s)
-      | _ -> e
-      in
       let break e = match e with
-      | FailError (0, _) -> false
-      | FailError (n, s) -> true
-      | _ -> false
+      | FailError (0, _) -> None
+      | FailError (n, s) -> Some (FailError (pred n, s))
+      | _ -> None
       in
       let tac = Proofview.tclBREAK break tac >>= fun ans -> interp_match_success ist ans in
       (** Once a tactic has succeeded, do not backtrack anymore *)
-      Proofview.tclONCE (Proofview.tclOR tac (fun e -> Proofview.tclZERO (decrease e)))
+      Proofview.tclONCE tac
 
 (* Interprets the Match expressions *)
 and interp_match ist lz constr lmr =