diff options
author | 2014-12-12 16:58:32 +0100 | |
---|---|---|
committer | 2014-12-12 19:23:16 +0100 | |
commit | 180af0dde65e4532cdeb13ec9aa43d8e83f7408f (patch) | |
tree | 745b35e71e0ba4124cd3418edba60488ce9856b8 /printing | |
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 'printing')
-rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 412c1050b..d43b94ec4 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1190,6 +1190,12 @@ module Make keyword "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t), ltactical + | TacIfThenCatch (t,tt,te) -> + hov 1 ( + str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + ltactical | TacOrelse (t1,t2) -> hov 1 ( pr_tac (lorelse,L) t1 ++ spc () |