Extension to the general sequence operator (tactical). Now in addition to the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0.

The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command
expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 107 insertions, 55 deletions

diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 890bb3ce5..aad3a765d 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -113,7 +113,7 @@ let count_subgoals2
 let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
     TacThens (a,l) ->
       (fun report_holder -> checked_thens report_holder a l)
-  | TacThen (a,b) ->
+  | TacThen (a,[||],b,[||]) ->
       (fun report_holder -> checked_then report_holder a b)
   | t ->
       (fun report_holder g ->
@@ -279,7 +279,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
       	| Failed n -> TacId []
       	| Tree_fail r -> reconstruct_success_tac a r
       	| Mismatch (n,p) -> a)
-  | TacThen (a,b) ->
+  | TacThen (a,[||],b,[||]) ->
       (function
 	  Report_node(true, n, l) -> tac
 	| Report_node(false, n, rl) ->
@@ -340,7 +340,7 @@ Tacinterp.add_tactic "OnThen" on_then;;
 
 let rec clean_path tac l = 
   match tac, l with
-  | TacThen (a,b), fst::tl ->
+  | TacThen (a,[||],b,[||]), fst::tl ->
       fst::(clean_path (if fst = 1 then a else b) tl)
   | TacThens (a,l), 1::tl ->
       1::(clean_path a tl)
@@ -390,7 +390,7 @@ let rec report_error
 	  | t::tl -> (report_error t the_goal the_ast returned_path (n::2::path))::
 	      (fold_num (n + 1) tl) in
 	fold_num 1 l)
-    | TacThen (a,b) ->
+    | TacThen (a,[||],b,[||]) ->
 	let the_count = ref 1 in
 	tclTHEN
 	  (fun g ->
@@ -398,7 +398,7 @@ let rec report_error
 	      report_error a the_goal the_ast returned_path (1::path) g
 	    with
 	      e ->
-		(the_ast := TacThen (!the_ast, b);
+		(the_ast := TacThen (!the_ast,[||], b,[||]);
 		 raise e))
 	  (fun g ->
 	    try
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index d2f71bfc2..b1809523c 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -156,7 +156,7 @@ let make_pbp_pattern x =
 let rec make_then = function
   | [] -> TacId []
   | [t] -> t
-  | t1::t2::l -> make_then (TacThen (t1,t2)::l)
+  | t1::t2::l -> make_then (TacThen (t1,[||],t2,[||])::l)
 
 let make_pbp_atomic_tactic = function
   | PbpTryAssumption None -> TacTry (TacAtom (zz, TacAssumption))
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 57116c070..6d52be45d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -775,10 +775,11 @@ and xlate_tactic =
    | TacFun (largs, t) ->
        let fst, rest =  xlate_largs_to_id_opt largs in
        CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
-   | TacThen (t1,t2) -> 
+   | TacThen (t1,[||],t2,[||]) -> 
        (match xlate_tactic t1 with
             CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
 	  | t -> CT_then (t,[xlate_tactic t2]))
+   | TacThen _ -> xlate_error "TacThen generalization TODO"
    | TacThens(t1,[]) -> assert false
    | TacThens(t1,t::l) ->
        let ct = xlate_tactic t in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index fb3c7940b..bdea94a04 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -131,7 +131,7 @@ GEXTEND Gram
     [ [ c = operconstr LEVEL "200" -> c ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "9" -> c ] ]
+    [ [ c = operconstr LEVEL "1" -> c ] ]
   ;
   operconstr:
     [ "200" RIGHTA
@@ -210,7 +210,7 @@ GEXTEND Gram
   appl_arg:
     [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
 	  (c,Some (loc,ExplByName id))
-      | c=constr -> (c,None) ] ]
+      | c=operconstr LEVEL "9" -> (c,None) ] ]
   ;
   atomic_constr:
     [ [ g=global -> CRef g
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 4b954b174..5755aee64 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -46,16 +46,31 @@ GEXTEND Gram
   GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg
           constr_may_eval;
 
+  tactic_then_last:
+    [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
+          Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta)
+      | -> [||] 
+    ] ]
+  ;
+  tactic_then_gen:
+    [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last)
+      | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l))
+      | ".."; l = tactic_then_last -> ([], Some (TacId [], l))
+      | ta = tactic_expr -> ([ta], None)
+      | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last)
+      | -> ([TacId []], None)
+    ] ]
+  ;
   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)
-      | ta = tactic_expr; ";"; 
-	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
-	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
-	  TacThens (ta, lta) ]
+      [ 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)
+	  | 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)
@@ -114,6 +129,7 @@ GEXTEND Gram
   (* Tactic arguments *)
   tactic_arg:
     [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a
+      | IDENT "ltac"; ":"; n = natural -> Integer n
       | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
       | a = may_eval_arg -> a
       | r = reference -> Reference r
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 495634512..a70c9acdb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -487,6 +487,17 @@ let pr_seq_body pr tl =
         prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
         str " ]")
 
+let pr_opt_tactic pr = function
+  | TacId [] -> mt ()
+  | t -> pr t
+
+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 ++
+        str " ]")
+
 let pr_hintbases = function
   | None -> spc () ++ str "with *"
   | Some [] -> mt ()
@@ -858,10 +869,14 @@ 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) ->
+      hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++
+             pr_then_gen (pr_tac ltop) tf t2 tl),
+      lseq
   | TacTry t ->
       hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t),
       ltactical
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 56dd32c55..bea93a39c 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -398,8 +398,8 @@ let rec mlexpr_of_atomic_tactic = function
 and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
   | Tacexpr.TacAtom (loc,t) ->
       <: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/proofs/refiner.ml b/proofs/refiner.ml
index a03e0b9e6..76fe0129f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -334,29 +334,25 @@ let start_tac gls =
 
 let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
 
-(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *)
-let thensf_tac taci tac (sigr,gs,p) =
-  let n = Array.length taci in
-  let nsg = List.length gs in
-  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
+  let nf = Array.length tacfi in
+  let nl = Array.length tacli in
+  let ng = List.length gs in
+  if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll,pl =
     List.split
-      (list_map_i (fun i -> apply_sig_tac sigr (if i<n then taci.(i) else tac))
+      (list_map_i (fun i -> 
+        apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
   (sigr, List.flatten gll,
    compose p (mapshape (List.map List.length gll) pl))
 
-(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *)
-let thensl_tac tac taci (sigr,gs,p) =
-  let n = Array.length taci in
-  let nsg = List.length gs in
-  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
-  let gll,pl =
-    List.split
-      (list_map_i (fun i -> apply_sig_tac sigr (if i<0 then tac else taci.(i)))
-	(n-nsg) gs) in
-  (sigr, List.flatten gll,
-   compose p (mapshape (List.map List.length gll) pl))
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thensf_tac taci tac = thens3parts_tac taci tac [||]
+
+(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *)
+let thensl_tac tac taci = thens3parts_tac [||] tac taci
 
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
 let thensi_tac tac (sigr,gs,p) =
@@ -382,19 +378,25 @@ let theni_tac i tac ((_,gl,_) as subgoals) =
       subgoals
   else non_existent_goal k 
 
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+   error if the number of resulting subgoals is strictly less than [n+m] *)
+let tclTHENS3PARTS tac1 tacfi tac tacli gls =
+  finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls)))
+
 (* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
-   to [gls] and applies [t1], ..., [tn] to the [n] first resulting
+   to [gls] and applies [t1], ..., [tn] to the first [n] resulting
    subgoals, and [tac2] to the others subgoals. Raises an error if
    the number of resulting subgoals is strictly less than [n] *)
-let tclTHENSFIRSTn tac1 taci tac gls =
-  finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls)))
+let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||]
 
 (* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
-   to [gls] and applies [t1], ..., [tn] to the [n] last resulting
+   to [gls] and applies [t1], ..., [tn] to the last [n] resulting
    subgoals, and [tac2] to the other subgoals. Raises an error if the
    number of resulting subgoals is strictly less than [n] *)
-let tclTHENSLASTn tac1 tac taci gls =
-  finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls)))
+let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
 
 (* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
    [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
@@ -407,13 +409,13 @@ let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
 
 (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
-let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2
+let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
 
 (* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
    [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
    an error if the number of resulting subgoals is not [n] *)
 let tclTHENSV tac1 tac2v =
-  tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.")
+  tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||]
 
 let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
 
@@ -425,7 +427,6 @@ let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
    to the first resulting subgoal *)
 let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
 
-
 (* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
    convenient than [tclTHEN] when [n] is large. *)
 let rec tclTHENLIST = function
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index b4b37fdf3..43d5af159 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -100,6 +100,13 @@ val tclTHENS         : tactic -> tactic list -> tactic
 val tclTHENST        : tactic -> tactic array -> tactic -> tactic
 *)
 
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+   error if the number of resulting subgoals is strictly less than [n+m] *)
+val tclTHENS3PARTS     : tactic -> tactic array -> tactic -> tactic array -> tactic
+
 (* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
    last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
 val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index caa7523a6..633a9a42d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -197,8 +197,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
-  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * 
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array *
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array
+  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * 
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 75f517023..e0c279a07 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -764,15 +764,21 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
   | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
-  | TacThen (t1,t2) ->
+  | TacThen (t1,[||],t2,[||]) ->
       let lfun', t1 = intern_tactic_seq ist t1 in
       let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
-      lfun'', TacThen (t1,t2)
+      lfun'', TacThen (t1,[||],t2,[||])
+  | TacThen (t1,tf,t2,tl) ->
+      let lfun', t1 = intern_tactic_seq 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_tactic ist') tf,intern_tactic ist' t2,
+		       Array.map (intern_tactic ist') tl)
   | TacThens (t,tl) ->
       let lfun', t = intern_tactic_seq ist t in
+      let ist' = { ist with ltacvars = lfun' } in
       (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun',
-      TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
+      lfun', TacThens (t, List.map (intern_tactic ist') tl)
   | TacDo (n,tac) -> 
       ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
   | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
@@ -1532,9 +1538,10 @@ and eval_tactic ist = function
   | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
   | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
-  | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
-  | TacThens (t,tl) ->
-      tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl)
+  | TacThen (t1,tf,t,tl) -> 
+      tclTHENS3PARTS (interp_tactic ist t1)
+	(Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl)
+  | TacThens (t1,tl) -> tclTHENS (interp_tactic ist t1) (List.map (interp_tactic ist) tl)
   | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTry tac -> tclTRY (interp_tactic ist tac)
   | TacInfo tac -> tclINFO (interp_tactic ist tac)
@@ -2410,8 +2417,9 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacId _ | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
-  | TacThen (t1,t2) ->
-      TacThen (subst_tactic subst t1,subst_tactic subst t2)
+  | 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)
   | TacThens (t,tl) ->
       TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
   | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)