diff options
| author | herbelin | 2000-01-07 22:27:11 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-07 22:27:11 +0000 |
| commit | 424bf8a5131aaf4960745c7050e5977c6e5fd4a5 (patch) | |
| tree | e23b22a6a106a7cbc0cd54cd48098f5c6aaceb68 /parsing | |
| parent | f5863b8f5a6c8791f089a2ddb43978a298394c95 (diff) | |
Renommage command en constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 2c8cb53dc3..3064492d33 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -34,10 +34,10 @@ GEXTEND Gram [ [ s = Prim.string -> s ] ] ; comarg: - [ [ c = Command.command -> <:ast< (COMMAND $c) >> ] ] + [ [ c = Constr.constr -> <:ast< (CONSTR $c) >> ] ] ; lcomarg: - [ [ c = Command.lcommand -> <:ast< (COMMAND $c) >> ] ] + [ [ c = Constr.lconstr -> <:ast< (CONSTR $c) >> ] ] ; lvernac: [ [ v = vernac; l = lvernac -> v::l @@ -54,9 +54,11 @@ GEXTEND Gram [ [ IDENT "Pwd"; "." -> <:ast< (PWD) >> | IDENT "Cd"; "." -> <:ast< (CD) >> | IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >> - | "Quit"; "." -> <:ast< (QUIT) >> + | IDENT "Drop"; "." -> <:ast< (DROP) >> - | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP) >> + | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP)>> + | "Quit"; "." -> <:ast< (QUIT) >> + | IDENT "Print"; IDENT "All"; "." -> <:ast< (PrintAll) >> | IDENT "Print"; "." -> <:ast< (PRINT) >> | IDENT "Print"; IDENT "Hint"; "*"; "." |