From 0fdd57f8db64b308b32e114fe5d6660f077a1664 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Jul 2010 11:37:40 +0000
Subject: Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a
 keyword).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13295 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 90df20979e..359d2321d3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -570,7 +570,7 @@ GEXTEND Gram
       | IDENT "Generalizable"; 
 	   gen = [IDENT "All"; IDENT "Variables" -> Some []
 	     | IDENT "No"; IDENT "Variables" -> None
-	     | [IDENT "Variable" | IDENT "Variables"];
+	     | ["Variable" | IDENT "Variables"];
 		  idl = LIST1 identref -> Some idl ] ->
 	     VernacGeneralizable (use_non_locality (), gen) ] ]
   ;
-- 
cgit v1.2.3