diff options
| author |  courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-09 15:01:30 +0000 |
|---|---|---|
| committer | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-09 15:01:30 +0000 |
| commit | 4f021dfa94a823bce9070fb36e8ec49a749e4a1c (patch) | |
| tree | d5e9712380e4eddac0b4bebd1b995f5b67fb46d6 /parsing | |
| parent | 01b8dc21e73e222dfe66488cf0a8a76fd0efdf10 (diff) | |
nettoyage d'entrees de grammaires inutiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1563 85f007b7-540e-0410-9357-904b9bb8a0f7
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 e42223f4b..f4edcd544 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 0ec5584fa..7ed3f645b 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; |