From 56a5d78e8dfecb46f4453c632c50e3270f7271bb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 22 Oct 2014 16:39:52 +0200
Subject: Specializing tclBREAK so that it can choose the return exception in
 case of a break.

---
 tactics/tacinterp.ml | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 443ec5aaed..2055bd7eab 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 =
-- 
cgit v1.2.3