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

3 files changed, 8 insertions, 7 deletions

diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 890bb3ce55..aad3a765de 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 d2f71bfc2f..b1809523c4 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 57116c0709..6d52be45d9 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