From 180af0dde65e4532cdeb13ec9aa43d8e83f7408f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 12 Dec 2014 16:58:32 +0100
Subject: 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.
---
 printing/pptactic.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'printing')

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 ()
-- 
cgit v1.2.3