Adding a tclBREAK primitive to the tactic monad.

1 files changed, 6 insertions, 0 deletions

diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 9ed3f4bd02..90b730198b 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -142,6 +142,12 @@ module Logical =
     let m = m s in
     { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
 
+  let break (f : exn -> bool) (m : 'a tactic) : 'a tactic = (); 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))
+    }
+
   type 'a reified = ('a, exn -> 'a reified) list_view IO.t
 
   let rec reflect (m : 'a reified) : 'a iolist =