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

1 files changed, 17 insertions, 9 deletions

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)