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.
---
 intf/tacexpr.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index efe62f569c..0c2b754788 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -251,6 +251,10 @@ and 'a gen_tactic_expr =
       'a gen_tactic_expr
   | TacExactlyOnce of
       'a gen_tactic_expr
+  | TacIfThenCatch of
+      'a gen_tactic_expr *
+      'a gen_tactic_expr *
+      'a gen_tactic_expr
   | TacOrelse of
       'a gen_tactic_expr *
       'a gen_tactic_expr
-- 
cgit v1.2.3