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].. ].

6 files changed, 57 insertions, 7 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d31908114..22ec1b445 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
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index dd7687f43..2d9cd3cd4 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 *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 2aadde7c1..0039a81bf 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -505,15 +505,28 @@ let pr_seq_body pr tl =
         prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
         str " ]")
 
+let pr_dispatch pr tl =
+  hv 0 (str "[>" ++
+        prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
+        str " ]")
+
 let pr_opt_tactic pr = function
   | TacId [] -> mt ()
   | t -> pr t
 
+let pr_tac_extend_gen pr tf tm tl =
+  prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
+  pr_opt_tactic pr tm ++ str ".." ++
+  prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl
+
 let pr_then_gen pr tf tm tl =
   hv 0 (str "[ " ++
-        prvect_with_sep mt (fun t -> pr t ++ spc () ++ str "| ") tf ++
-	pr_opt_tactic pr tm ++ str ".." ++
-	prvect_with_sep mt (fun t -> spc () ++ str "| " ++ pr t) tl ++
+        pr_tac_extend_gen pr tf tm tl ++
+        str " ]")
+
+let pr_tac_extend pr tf tm tl =
+  hv 0 (str "[>" ++
+        pr_tac_extend_gen pr tf tm tl ++
         str " ]")
 
 let pr_hintbases = function
@@ -851,6 +864,8 @@ let rec pr_tac inherited tac =
       hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
              pr_tac (lseq,L) t2),
       lseq
+  | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl , lseq
+  | TacExtendTac (tf,t,tr) -> pr_tac_extend (pr_tac ltop) tf t tr , lseq
   | TacThens3parts (t1,tf,t2,tl) ->
       hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
              pr_then_gen (pr_tac ltop) tf t2 tl),
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 324ea2f04..2a66b32bc 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -593,6 +593,13 @@ and intern_tactic_seq onlytac ist = function
       let lfun', t1 = intern_tactic_seq onlytac ist t1 in
       let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in
       lfun'', TacThen (t1,t2)
+  | TacDispatch tl ->
+      ist.ltacvars , TacDispatch (List.map (intern_pure_tactic ist) tl)
+  | TacExtendTac (tf,t,tl) ->
+      ist.ltacvars ,
+      TacExtendTac (Array.map (intern_pure_tactic ist) tf,
+                    intern_pure_tactic ist t,
+		    Array.map (intern_pure_tactic ist) tl)
   | TacThens3parts (t1,tf,t2,tl) ->
       let lfun', t1 = intern_tactic_seq onlytac ist t1 in
       let ist' = { ist with ltacvars = lfun' } in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1eecb9497..20234d1f2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1042,6 +1042,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       end
   | TacThen (t1,t) ->
       Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
+  | TacDispatch tl ->
+      Proofview.tclDISPATCH (List.map (interp_tactic ist) tl)
+  | TacExtendTac (tf,t,tl) ->
+      Proofview.tclEXTEND (Array.map_to_list (interp_tactic ist) tf)
+                          (interp_tactic ist t)
+                          (Array.map_to_list (interp_tactic ist) tl)
   | TacThens (t1,tl) -> Tacticals.New.tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
   | TacThens3parts (t1,tf,t,tl) ->
       Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index ecadfca59..30fffed91 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -225,6 +225,11 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
   | TacThen (t1,t2) ->
       TacThen (subst_tactic subst t1, subst_tactic subst t2)
+  | TacDispatch tl -> TacDispatch (List.map (subst_tactic subst) tl)
+  | TacExtendTac (tf,t,tl) ->
+      TacExtendTac (Array.map (subst_tactic subst) tf,
+	            subst_tactic subst t,
+                    Array.map (subst_tactic subst) tl)
   | TacThens (t,tl) ->
       TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
   | TacThens3parts (t1,tf,t2,tl) ->