diff options
| author | herbelin | 2000-10-17 13:34:42 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-17 13:34:42 +0000 |
| commit | da3802b2a23f852e6c1466224188f6dd41faa683 (patch) | |
| tree | 30ed9f107ee6b0c376d15aa071cc3a336dbcfdc5 | |
| parent | 8aa10dc916cb186d8e229cce08167b756a1522c7 (diff) | |
Pb factorisation de Print Grammar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@713 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_basevernac.ml4 | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 03af08edc8..1dfc5790f5 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -71,6 +71,10 @@ GEXTEND Gram | IDENT "Print"; IDENT "Section"; s = identarg; "." -> <: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) >> + | IDENT "Locate"; IDENT "File"; f = stringarg; "." -> <:ast< (LocateFile $f) >> | IDENT "Locate"; IDENT "Library"; id = identarg; "." -> @@ -205,8 +209,8 @@ GEXTEND Gram p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >> | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string; p = identarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >> - | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." -> - <:ast< (PrintGrammar $uni $ent) >> + (* "Print" "Grammar" should be here but is in "command" entry in order + to factorize with other "Print"-based vernac entries *) ] ] ; |