diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:50:11 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:50:11 +0200 |
| commit | 4e2f3ff7d2f790435c9e1d3dfc4f26beff47ae8a (patch) | |
| tree | 12243f22532754ff89addf963679d034184e3602 /parsing | |
| 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')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/highparsing.mllib | 4 | ||||
| -rw-r--r-- | parsing/parsing.mllib | 4 |
3 files changed, 6 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5b044d2f0..de98415cd 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 *) diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib deleted file mode 100644 index 05e2911c2..000000000 --- a/parsing/highparsing.mllib +++ /dev/null @@ -1,4 +0,0 @@ -G_constr -G_vernac -G_prim -G_proofs diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 2a73d7bc6..1f29636b2 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -3,3 +3,7 @@ CLexer Pcoq Egramml Egramcoq +G_constr +G_vernac +G_prim +G_proofs |