From 3bb0fa9596316e2a049df646e08bafbffc9691ad Mon Sep 17 00:00:00 2001
From: puech
Date: Tue, 3 Feb 2009 19:18:25 +0000
Subject: Do not reserve the keyword "Infer".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11879 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 03b1466481..7f4a995424 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -220,7 +220,7 @@ GEXTEND Gram
       | "CoInductive" -> (CoInductive,CoFinite) ] ]
   ;
   infer_token:
-    [ [ "Infer" -> true | -> false ] ]
+    [ [ IDENT "Infer" -> true | -> false ] ]
   ;
   record_token:
     [ [ IDENT "Record" -> (Record,BiFinite)
-- 
cgit v1.2.3