From f30822ba46d08d65597e0e3230ea6ad86c98453f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 7 Nov 2016 16:03:53 +0100
Subject: Proofview: tclINDEPENDENTL

---
 tactics/tacticals.ml  | 13 +++++++++++++
 tactics/tacticals.mli |  1 +
 2 files changed, 14 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 93c04e373c..c5562b326c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -368,6 +368,16 @@ module New = struct
           catch_failerror e <*> t2
         end
     end
+
+  let tclORELSE0L t1 t2 =
+    tclINDEPENDENTL begin
+      tclORELSE
+        t1
+        begin fun e ->
+          catch_failerror e <*> t2
+        end
+    end
+
   let tclORELSE t1 t2 =
     tclORELSE0 (tclPROGRESS t1) t2
 
@@ -419,6 +429,9 @@ module New = struct
 
   let tclTRY t =
     tclORELSE0 t (tclUNIT ())
+  
+  let tclTRYb t =
+    tclORELSE0L (t <*> tclUNIT true) (tclUNIT false)
 
   let tclIFTHENELSE t1 t2 t3 =
     tclINDEPENDENT begin
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 18cf03c51d..7aacc52f33 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -209,6 +209,7 @@ module New : sig
   val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic
 
   val tclTRY : unit tactic -> unit tactic
+  val tclTRYb : unit tactic -> bool list tactic
   val tclFIRST : unit tactic list -> unit tactic
   val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
   val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
-- 
cgit v1.2.3