diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-12-12 16:58:32 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-12-12 19:23:16 +0100 |
| commit | 180af0dde65e4532cdeb13ec9aa43d8e83f7408f (patch) | |
| tree | 745b35e71e0ba4124cd3418edba60488ce9856b8 /tactics/tacticals.mli | |
| parent | a5ccde6f22deb1a1a2d59d3b532f74c217a05aee (diff) | |
Add Ltac syntax for the [tclIFCATCH] primitive.
[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 35a320589..fbdc6d94e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -176,6 +176,12 @@ module New : sig val tclONCE : unit tactic -> unit tactic val tclEXACTLY_ONCE : unit tactic -> unit tactic + + val tclIFCATCH : + unit tactic -> + (unit -> unit tactic) -> + (unit -> unit tactic) -> unit tactic + val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |