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.
---
 parsing/g_ltac.ml4 | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'parsing')

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