Distinguish tactics t1;t2 and t1;[t2..].

They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently.

7 files changed, 27 insertions, 23 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 648407a707..360b96dc4a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -427,8 +427,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
   | Tacexpr.TacAtom (loc,t) ->
       let loc = of_coqloc loc in
       <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >>
-  | Tacexpr.TacThen (t1,[||],t2,[||]) ->
-      <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ [||] $mlexpr_of_tactic t2$ [||]>>
+  | Tacexpr.TacThen (t1,t2) ->
+      <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$>>
   | Tacexpr.TacThens (t,tl) ->
       <:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>>
   | Tacexpr.TacFirst tl ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 493c0939a5..d5a3328f02 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -187,12 +187,15 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
   | TacAtom of Loc.t * ('t,'p,'c,'i,'r,'n,'l) gen_atomic_tactic_expr
   | TacThen of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
-      ('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
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacThens of
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
       ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list
+  | TacThens3parts of
+      ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr *
+      ('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
   | TacFirst of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list
   | TacComplete of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
   | TacSolve of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index fd7091ec9d..5f82cf5f26 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -54,11 +54,11 @@ GEXTEND Gram
     [ "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; ";"; 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) -> TacThen (ta0, Array.of_list first, t, last)
+	  | Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last)
 	  | None -> TacThens (ta0,first) ]
     | "3" RIGHTA
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e51d7b3fd9..90341a69b8 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -846,11 +846,11 @@ let rec pr_tac inherited tac =
       hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++
              pr_seq_body (pr_tac ltop) tl),
       lseq
-  | TacThen (t1,[||],t2,[||]) ->
+  | TacThen (t1,t2) ->
       hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
              pr_tac (lseq,L) t2),
       lseq
-  | TacThen (t1,tf,t2,tl) ->
+  | TacThens3parts (t1,tf,t2,tl) ->
       hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
              pr_then_gen (pr_tac ltop) tf t2 tl),
       lseq
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index bcff61e9c1..56adcc1783 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -591,15 +591,15 @@ and intern_tactic_seq onlytac ist = function
   | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
   | TacAbstract (tac,s) ->
       ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
-  | TacThen (t1,[||],t2,[||]) ->
+  | TacThen (t1,t2) ->
       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,[||])
-  | TacThen (t1,tf,t2,tl) ->
+      lfun'', TacThen (t1,t2)
+  | TacThens3parts (t1,tf,t2,tl) ->
       let lfun', t1 = intern_tactic_seq onlytac ist t1 in
       let ist' = { ist with ltacvars = lfun' } in
       (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun', TacThen (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2,
+      lfun', TacThens3parts (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2,
 		       Array.map (intern_pure_tactic ist') tl)
   | TacThens (t,tl) ->
       let lfun', t = intern_tactic_seq true ist t in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bc7e02ed43..3bccbf41fc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1014,13 +1014,12 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
         (Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac)
       end
-  | TacThen (t1,tf,t,tl) ->
-      if Array.length tf = 0 && Array.length tl = 0 then
-        Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
-      else
-        Tacticals.New.tclTHENS3PARTS (interp_tactic ist t1)
-	  (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
+  | TacThen (t1,t) ->
+      Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
   | 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)
+	(Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
   | TacDo (n,tac) -> Tacticals.New.tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTime (s,tac) -> Tacticals.New.tclTIME s (interp_tactic ist tac)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d603561054..0d8923d5ba 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -223,11 +223,13 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
-  | TacThen (t1,tf,t2,tl) ->
-      TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
-	       subst_tactic subst t2,Array.map (subst_tactic subst) tl)
+  | TacThen (t1,t2) ->
+      TacThen (subst_tactic subst t1, subst_tactic subst t2)
   | TacThens (t,tl) ->
       TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
+  | TacThens3parts (t1,tf,t2,tl) ->
+      TacThens3parts (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
+	       subst_tactic subst t2,Array.map (subst_tactic subst) tl)
   | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
   | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
   | TacTime (s,tac) -> TacTime (s,subst_tactic subst tac)