diff options
| -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 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 -> |