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/tacintern.ml | |
| 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/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 7d609e1a5..c0e18c1f2 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -654,6 +654,12 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacOnce (intern_pure_tactic ist tac) | TacExactlyOnce tac -> ist.ltacvars, TacExactlyOnce (intern_pure_tactic ist tac) + | TacIfThenCatch (tac,tact,tace) -> + ist.ltacvars, + TacIfThenCatch ( + intern_pure_tactic ist tac, + intern_pure_tactic ist tact, + intern_pure_tactic ist tace) | TacOrelse (tac1,tac2) -> ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) |