diff options
| author | letouzey | 2012-07-11 16:50:17 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-11 16:50:17 +0000 |
| commit | 66483fbbb6549bc57bd409c689ee7d99e4d45d9d (patch) | |
| tree | 3e68c2f682ad5a55cd1c4a33b89fc954f4bbf99f /parsing | |
| parent | df954f17d5f487e06ee21e10bab1ae9a133ba72d (diff) | |
Re-allow Reset in compiled files
This was a wish by A. Chlipala on coq-club
Both Reset foo and Reset Initial are accepted (with a warning).
If some proofs were opened, all of them are aborted. This isn't the
behavior of the interactive Reset that has more information and can
be more selective, but this shouldn't be a big issue in practice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15597 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 40cf0d06d9..043d2097b9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -938,8 +938,8 @@ GEXTEND Gram | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s (* Resetting *) - | IDENT "Reset"; id = identref -> VernacResetName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial + | IDENT "Reset"; id = identref -> VernacResetName id | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n | IDENT "BackTo"; n = natural -> VernacBackTo n |