Proofview: tclINDEPENDENTL

2 files changed, 14 insertions, 0 deletions

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