diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-13 17:51:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-13 17:51:19 +0000 |
| commit | 42c93f15c135af0e5c822d2a60fbb92002acb2ca (patch) | |
| tree | e350420bb71e1005bedf556adfde00424590cdc2 /parsing | |
| parent | 10cd7b645008f9390009ba5a07331b56e1f08ec5 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 79500c236..c40cabbd8 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 -> |