From 2925c97c852efd66656edebedba543c7c8335b73 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 31 Jul 2014 16:08:27 +0200
Subject: New tactical [> t1…tn] to apply tactics t1…tn to the corresponding
 goal.

Differs from the usual t;[t1…tn] in two ways:
* It can be used without a preceding tactic
* It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals.

In other words t;[t1…tn] is [> t;[>t1…tn].. ].---
 intf/tacexpr.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d319081145..22ec1b4459 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -197,6 +197,12 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacThen of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
+  | TacDispatch of
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list
+  | TacExtendTac of
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr array *
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr array
   | TacThens of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list
-- 
cgit v1.2.3