Added syntax "exists bindings, ..., bindings" for iterated "exists".

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

14 files changed, 33 insertions, 24 deletions

diff --git a/CHANGES b/CHANGES
index 31fb1453c..17bade57b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,6 +29,8 @@ Tactics
 - New variant "subst'" of "subst" that supports JMeq.
 - New tactic "decide lemma with hyp" for rewriting decidability lemmas
   when one knows which side is true.
+- Tactic "exists" and "eexists" supports iteration using
+  comma-separated arguments.
 
 Tactic Language
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d3d1ad918..abc294e8b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1515,6 +1515,10 @@ equivalent to {\tt intros; apply ci}.
   case of existential quantification $\exists x\cdot P(x)$. 
   Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}.
 
+\item {\tt exists \nelist{\bindinglist}{,}}
+
+  This iteratively applies {\tt exists {\bindinglist}}.
+
 \item {\tt left}\tacindex{left}\\
       {\tt right}\tacindex{right}
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d5d32ce5b..875b9dc07 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -602,10 +602,11 @@ GEXTEND Gram
       | IDENT "eleft";  bl = with_bindings -> TacLeft  (true,bl)
       | IDENT "right";  bl = with_bindings -> TacRight (false,bl)
       | IDENT "eright"; bl = with_bindings -> TacRight (true,bl)
-      | IDENT "split";  bl = with_bindings -> TacSplit (false,false,bl)
-      | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl)
-      | "exists";        bl = opt_bindings -> TacSplit (false,true,bl)
-      | IDENT "eexists"; bl = opt_bindings -> TacSplit (true,true,bl)
+      | IDENT "split";  bl = with_bindings -> TacSplit (false,false,[bl])
+      | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl])
+      | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll)
+      | IDENT "eexists"; bll = LIST1 opt_bindings SEP "," ->
+	  TacSplit (true,true,bll)
       | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (false,n,l)
       | IDENT "econstructor"; n = num_or_meta; l = with_bindings ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index bdd9241e3..bed5e1b28 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -819,8 +819,8 @@ and pr_atom1 = function
   (* Constructors *)
   | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l)
   | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l)
-  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ pr_bindings l)
-  | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ pr_ex_bindings l)
+  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_coma pr_bindings l)
+  | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep pr_coma pr_ex_bindings l)
   | TacAnyConstructor (ev,Some t) ->
       hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t)
   | TacAnyConstructor (ev,None) as t -> pr_atom0 t
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 606b652c2..91cb681a5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -394,7 +394,7 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>>
   | Tacexpr.TacSplit (ev,b,l) ->
       <:expr< Tacexpr.TacSplit
-        ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>>
+        ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>>
   | Tacexpr.TacAnyConstructor (ev,t) ->
       <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>>
   | Tacexpr.TacConstructor (ev,n,l) ->
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 9e649a5a2..83c156f7b 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -342,8 +342,9 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     (* Constructors *)
     | TacLeft        (_,cb)
     | TacRight       (_,cb)
-    | TacSplit       (_, _, cb)
+    | TacSplit       (_, _, [cb])
     | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
+    | TacSplit       _ -> failwith "TODO"
     | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc
 
     (* Conversion *)
diff --git a/plugins/interface/pbp.ml b/plugins/interface/pbp.ml
index 01747aa58..663e4ce92 100644
--- a/plugins/interface/pbp.ml
+++ b/plugins/interface/pbp.ml
@@ -163,7 +163,7 @@ let make_pbp_atomic_tactic = function
   | PbpTryAssumption (Some a) ->
       TacTry (TacAtom (zz, TacExact (make_var a)))
   | PbpExists x -> 
-      TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
+      TacAtom (zz, TacSplit (false,true,[ImplicitBindings [make_pbp_pattern x]]))
   | PbpGeneralize (h,args) ->
       let l = List.map make_pbp_pattern args in
       TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous])
@@ -178,7 +178,7 @@ let make_pbp_atomic_tactic = function
 	(zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
       TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
-  | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));;
+  | PbpSplit -> TacAtom (zz, TacSplit (false,false,[NoBindings]));;
 
 let rec make_pbp_tactic = function
   | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl)
diff --git a/plugins/interface/showproof.ml b/plugins/interface/showproof.ml
index 2ab62763d..aa11609ae 100644
--- a/plugins/interface/showproof.ml
+++ b/plugins/interface/showproof.ml
@@ -1183,8 +1183,8 @@ let rec natural_ntree ig ntree =
 	    TacIntroPattern _ -> natural_intros ig lh g gs ltree
 	  | TacIntroMove _ -> natural_intros ig lh g gs ltree
 	  | TacFix (_,n) -> natural_fix ig lh g gs n ltree
-	  | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree
-	  | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
+	  | TacSplit (_,_,[NoBindings]) -> natural_split ig lh g gs ge [] ltree
+	  | TacSplit(_,_,[ImplicitBindings l]) -> natural_split ig lh g gs ge (List.map snd l) ltree
 	  | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree
 	  | TacRight _ -> natural_right ig lh g gs ltree
 	  | TacLeft _ -> natural_left ig lh g gs ltree
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index c27b10c63..4d4eff56f 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -996,8 +996,8 @@ and xlate_tac =
     | TacIntroMove _ -> xlate_error "TODO"
     | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
     | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
-    | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
-    | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl)
+    | TacSplit (false,false,[bindl]) -> CT_split (xlate_bindings bindl)
+    | TacSplit (false,true,[bindl]) -> CT_exists (xlate_bindings bindl)
     | TacSplit _ | TacRight _ | TacLeft _ -> 
 	xlate_error "TODO: esplit, eright, etc"
     | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 65b330c3d..f53327249 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -197,7 +197,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Constructors *)
   | TacLeft of evars_flag * 'constr bindings
   | TacRight of evars_flag * 'constr bindings
-  | TacSplit of evars_flag * split_flag * 'constr bindings
+  | TacSplit of evars_flag * split_flag * 'constr bindings list
   | TacAnyConstructor of evars_flag * 'tac option
   | TacConstructor of evars_flag * int or_metaid * 'constr bindings
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 6f592108b..e0c267c07 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -98,7 +98,7 @@ val h_revert          : identifier list -> tactic
 val h_constructor     : evars_flag -> int -> open_constr bindings -> tactic
 val h_left            : evars_flag -> open_constr bindings -> tactic
 val h_right           : evars_flag -> open_constr bindings -> tactic
-val h_split           : evars_flag -> open_constr bindings -> tactic
+val h_split           : evars_flag -> open_constr bindings list -> tactic
 
 val h_one_constructor : int -> tactic
 val h_simplest_left   : tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9da5678cf..5df025c1a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -198,8 +198,8 @@ let _ =
         "eleft", TacLeft(true,NoBindings);
         "right", TacRight(false,NoBindings);
         "eright", TacRight(true,NoBindings);
-        "split", TacSplit(false,false,NoBindings);
-        "esplit", TacSplit(true,false,NoBindings);
+        "split", TacSplit(false,false,[NoBindings]);
+        "esplit", TacSplit(true,false,[NoBindings]);
         "constructor", TacAnyConstructor (false,None);
         "econstructor", TacAnyConstructor (true,None);
         "reflexivity", TacReflexivity;
@@ -777,7 +777,7 @@ let rec intern_atomic lf ist x =
   (* Constructors *)
   | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
   | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
-  | TacSplit (ev,b,bl) -> TacSplit (ev,b,intern_bindings ist bl)
+  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll)
   | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl)
 
@@ -2325,7 +2325,7 @@ and interp_atomic ist gl = function
   (* Constructors *)
   | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl)
   | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl)
-  | TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl)
+  | TacSplit (ev,_,bll) -> h_split ev (List.map (interp_bindings ist gl) bll)
   | TacAnyConstructor (ev,t) ->
       abstract_tactic (TacAnyConstructor (ev,t))
         (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
@@ -2649,7 +2649,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Constructors *)
   | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
   | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
-  | TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl)
+  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (subst_bindings subst) bll)
   | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 663c426f9..1ac95f728 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1166,7 +1166,8 @@ let any_constructor with_evars tacopt gl =
 
 let left_with_ebindings  with_evars = constructor_tac with_evars (Some 2) 1
 let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2
-let split_with_ebindings with_evars = constructor_tac with_evars (Some 1) 1
+let split_with_ebindings with_evars =
+  tclMAP (constructor_tac with_evars (Some 1) 1)
 
 let left l             = left_with_ebindings false (inj_ebindings l)
 let simplest_left      = left NoBindings
@@ -1174,7 +1175,7 @@ let simplest_left      = left NoBindings
 let right l            = right_with_ebindings false (inj_ebindings l)
 let simplest_right     = right NoBindings
 
-let split l            = split_with_ebindings false (inj_ebindings l)
+let split l            = split_with_ebindings false [inj_ebindings l]
 let simplest_split     = split NoBindings
 
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6e52546f4..ee2250b34 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -324,7 +324,7 @@ val split                : constr bindings -> tactic
 
 val left_with_ebindings  : evars_flag -> open_constr bindings -> tactic
 val right_with_ebindings : evars_flag -> open_constr bindings -> tactic
-val split_with_ebindings : evars_flag -> open_constr bindings -> tactic
+val split_with_ebindings : evars_flag -> open_constr bindings list -> tactic
 
 val simplest_left        : tactic
 val simplest_right       : tactic