diff options
Diffstat (limited to 'parsing/g_vernacnew.ml4')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index cf89300bba..d62d40d33b 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -675,10 +675,9 @@ GEXTEND Gram modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (local,(op,modl),p,Some(op,modl),sc) - | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr; - l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing] - | -> [] ] -> - VernacNotation (local,c,Some("'"^s^"'",l),Some("'"^s^"'",l),None) + | 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 ] -> |