From 42c93f15c135af0e5c822d2a60fbb92002acb2ca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 13 Feb 2004 17:51:19 +0000
Subject: Uniformisation du comportement de Notation et Reserved Notation

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 79500c2366..c40cabbd85 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -673,14 +673,14 @@ GEXTEND Gram
 	 op = ne_string; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (local,(op,modl),p,Some(op,modl),sc)
+         VernacInfix (local,(op,modl),p,None,sc)
      | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
            VernacSyntacticDefinition (id,c,local,b)
      | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (local,c,Some(s,modl),Some(s,modl),sc)
+           VernacNotation (local,c,Some(s,modl),None,sc)
 
      | IDENT "Tactic"; IDENT "Notation"; s = ne_string; 
 	 pil = LIST0 production_item; ":="; t = Tactic.tactic -> 
-- 
cgit v1.2.3