diff options
| author | Maxime Dénès | 2017-09-15 10:50:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-15 10:50:11 +0200 |
| commit | 4e2f3ff7d2f790435c9e1d3dfc4f26beff47ae8a (patch) | |
| tree | 12243f22532754ff89addf963679d034184e3602 /parsing/g_vernac.ml4 | |
| parent | 9e6b192adcaadcdb1935a68f39ce5ea877562188 (diff) | |
| parent | 028de158153de94adfcb9d1e995259d833968951 (diff) | |
Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the top of the linking chain.
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5b044d2f04..de98415cd6 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1134,14 +1134,13 @@ GEXTEND Gram | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> - Metasyntax.check_infix_modifiers l; let (loc,s) = s in - VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l)) + VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l)) | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,(s,l)) + -> VernacSyntaxExtension (false, local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) |