From 351d36fc34c8e106e3072c723423d0a5cf72c7a0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Nov 2003 18:56:27 +0000
Subject: Pas d'entrees autres que les predefinies en v8

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8ee5c85e09..290a1be0e7 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -726,7 +726,6 @@ GEXTEND Gram
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
-      | e=IDENT -> ETOther("constr",e)
     ] ]
   ;
   opt_scope:
-- 
cgit v1.2.3