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.

3 files changed, 14 insertions, 13 deletions

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)