diff options
| author | filliatr | 1999-12-10 14:51:04 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-10 14:51:04 +0000 |
| commit | 1f2ec6429da2b09b58480c35e175428e39c1c37b (patch) | |
| tree | 0b0149b5dd52c524ae7601d19b667fa1ea8f064a /parsing | |
| parent | ba569318fee9055745b6bc191d97add351900e74 (diff) | |
- erreurs Pretype
- Write / Restore State
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 96b226be4b..4fb5380f54 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -311,26 +311,23 @@ GEXTEND Gram END -(* State management *) GEXTEND Gram vernac: [ [ - IDENT "Save"; IDENT "State"; id = identarg; "." -> - <:ast< (SaveState $id "") >> - | IDENT "Save"; IDENT "State"; id = identarg; s = stringarg; "." -> - <:ast< (SaveState $id $s) >> - | IDENT "Write"; IDENT "States"; id = identarg; "." -> - <:ast< (WriteStates $id) >> - | IDENT "Write"; IDENT "States"; id = stringarg; "." -> - <:ast< (WriteStates $id) >> + +(* State management *) + IDENT "Write"; IDENT "State"; id = identarg; "." -> + <:ast< (WriteState $id) >> + | IDENT "Write"; IDENT "State"; s = stringarg; "." -> + <:ast< (WriteState $s) >> | IDENT "Restore"; IDENT "State"; id = identarg; "." -> <:ast< (RestoreState $id) >> - | IDENT "Remove"; IDENT "State"; id = identarg; "." -> - <:ast< (RemoveState $id) >> + | IDENT "Restore"; IDENT "State"; s = stringarg; "." -> + <:ast< (RestoreState $s) >> + | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >> | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >> | IDENT "Reset"; IDENT "Section"; id = identarg; "." -> <:ast< (ResetSection $id) >> - | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >> (* Modules and Sections *) |