From 66483fbbb6549bc57bd409c689ee7d99e4d45d9d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 11 Jul 2012 16:50:17 +0000
Subject: 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
---
 parsing/g_vernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3