diff options
| -rw-r--r-- | tactics/tacticals.ml | 9 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 15 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 97e2373b7..9256e10d6 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -326,6 +326,15 @@ module New = struct end end + let tclORD t1 t2 = + tclINDEPENDENT begin + Proofview.tclOR + t1 + begin fun e -> + catch_failerror e <*> t2 () + end + end + let tclONCE = Proofview.tclONCE let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index d6630bb79..35a320589 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -169,6 +169,11 @@ module New : sig (** Fail with a [User_Error] containing the given message. *) val tclOR : unit tactic -> unit tactic -> unit tactic + val tclORD : unit tactic -> (unit -> unit tactic) -> unit tactic + (** Like {!tclOR} but accepts a delayed tactic as a second argument + in the form of a function which will be run only in case of + backtracking. *) + val tclONCE : unit tactic -> unit tactic val tclEXACTLY_ONCE : unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c28295b0f..f1b542481 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1911,7 +1911,7 @@ let one_constructor i lbind = constructor_tac false None i lbind let rec tclANY tac = function | [] -> Tacticals.New.tclZEROMSG (str "No applicable tactic.") | arg :: l -> - Proofview.tclOR (tac arg) (fun _ -> tclANY tac l) + Tacticals.New.tclORD (tac arg) (fun () -> tclANY tac l) let any_constructor with_evars tacopt = let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in |