From 525094414bf74445f930e170a823a49107726f6f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 May 2014 13:30:38 +0200
Subject: Fixing commit 9cef834. The parsing rules were generating an empty
 list, conflicting with the previous behaviour of 'eexists'.

---
 parsing/g_tactic.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 348722c849..7b79d7882c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -310,7 +310,7 @@ GEXTEND Gram
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
   ;
   opt_bindings:
-    [ [ bl = bindings -> bl | -> NoBindings ] ]
+    [ [ bl = LIST1 bindings SEP "," -> bl | -> [NoBindings] ] ]
   ;
   constr_with_bindings:
     [ [ c = constr; l = with_bindings -> (c, l) ] ]
@@ -628,8 +628,8 @@ GEXTEND Gram
       (* Constructors *)
       | IDENT "split";  bl = with_bindings -> TacSplit (false,false,[bl])
       | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl])
-      | "exists"; bll = LIST0 bindings SEP "," -> TacSplit (false,true,bll)
-      | IDENT "eexists"; bll = LIST0 bindings SEP "," ->
+      | "exists"; bll = opt_bindings -> TacSplit (false,true,bll)
+      | IDENT "eexists"; bll = opt_bindings ->
 	  TacSplit (true,true,bll)
       | IDENT "constructor"; n = nat_or_var; l = with_bindings ->
 	  TacConstructor (false,n,l)
-- 
cgit v1.2.3