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

4 files changed, 10 insertions, 9 deletions

diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 6f592108b1..e0c267c071 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 9da5678cf0..5df025c1a2 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 663c426f97..1ac95f7285 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 6e52546f4a..ee2250b346 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