aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/pptactic.ml')
-rw-r--r--printing/pptactic.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 412c1050b4..d43b94ec4b 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 ()