diff options
| author | Arnaud Spiwack | 2014-12-12 16:58:32 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-12 19:23:16 +0100 |
| commit | 180af0dde65e4532cdeb13ec9aa43d8e83f7408f (patch) | |
| tree | 745b35e71e0ba4124cd3418edba60488ce9856b8 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index de8d332b8b..b2b1d5adea 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -84,6 +84,9 @@ GEXTEND Gram | "2" RIGHTA [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) + | IDENT "tryif" ; ta = tactic_expr ; + "then" ; tat = tactic_expr ; + "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA |