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

1 files changed, 2 insertions, 2 deletions

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)