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, 8 insertions, 7 deletions

diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 9e649a5a2f..83c156f7bf 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 01747aa58f..663e4ce925 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 2ab62763d4..aa11609ae7 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 c27b10c63e..4d4eff56fb 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]) ->