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].. ].---
 parsing/g_ltac.ml4 | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index dd7687f430..2d9cd3cd41 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -50,16 +50,22 @@ GEXTEND Gram
       | -> ([TacId []], None)
     ] ]
   ;
+  tactic_then_locality: (* [true] for the local variant [TacThens] and [false]
+                           for [TacExtend] *)
+  [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ]
+  ;
   tactic_expr:
     [ "5" RIGHTA
       [ te = binder_tactic -> te ]
     | "4" LEFTA
       [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
       | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1)
-      | ta0 = tactic_expr; ";"; "["; (first,tail) = tactic_then_gen; "]" ->
-	  match tail with
-	  | Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
-	  | None -> TacThens (ta0,first) ]
+      | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" ->
+	  match l , tail with
+          | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
+	  | true  , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
+          | false , None -> TacThen (ta0,TacDispatch first)
+	  | true  , None -> TacThens (ta0,first) ]
     | "3" RIGHTA
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
       | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
@@ -107,6 +113,11 @@ GEXTEND Gram
           TacArg(!@loc,TacCall (!@loc,r,la)) ]
     | "0"
       [ "("; a = tactic_expr; ")" -> a
+      | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
+          begin match tail with
+          | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
+          | None -> TacDispatch tf
+          end
       | a = tactic_atom -> TacArg (!@loc,a) ] ]
   ;
   (* binder_tactic: level 5 of tactic_expr *)
-- 
cgit v1.2.3