diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index e42223f4b6..f4edcd5440 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -102,7 +102,6 @@ GEXTEND Gram <:ast< (PrintHintDb $s) >> | IDENT "Print"; IDENT "Section"; s = qualidarg -> <:ast< (PrintSec $s) >> - | IDENT "Print"; IDENT "States" -> <:ast< (PrintStates) >> (* This should be in "syntax" section but is here for factorization *) | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg -> <:ast< (PrintGrammar $uni $ent) >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0ec5584faf..7ed3f645b1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -404,7 +404,7 @@ GEXTEND Gram [ [ "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ]; s = [ s = STRING -> s | s = IDENT -> s ] -> <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >> - | "Compile"; +(* | "Compile"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ]; @@ -417,6 +417,7 @@ GEXTEND Gram let fname = match fname with Some s -> s | None -> mname in <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec) ($STR $mname) ($STR $fname))>> +*) | IDENT "Read"; IDENT "Module"; id = identarg -> <:ast< (ReadModule $id) >> | IDENT "Require"; import = import_tok; specif = specif_tok; |