From 51bf8ac5bc08bf9acd131c17c025c6ed6960ab89 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Nov 2002 12:15:29 +0000
Subject: Retablissement Syntactic Definition

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7a8f824780..1d7519c99f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -403,11 +403,10 @@ GEXTEND Gram
 	  Pp.warning "Class is obsolete"; VernacNop
 
 (* Implicit *)
-(*
       | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   VernacSyntacticDefinition (id,c,n)
-*)
+(*
       | IDENT "Syntactic"; "Definition"; id = IDENT; ":="; c = constr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   let c = match n with
@@ -416,7 +415,7 @@ GEXTEND Gram
 		 CApp (loc,c,l)
 	     | None -> c in
 	   VernacNotation ("'"^id^"'",c,[],None)
-
+*)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
-- 
cgit v1.2.3