From c51a32a5f3825dfd78212c976fb0d2d62b4e7d71 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 26 Jan 2012 16:06:14 +0000
Subject: Fail: discard the effects of a successful command (fix #2682)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14945 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 84e20f5eda..cbd95a4fb9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -206,7 +206,9 @@ let rec vernac_com interpfun (loc,com) =
 
     | VernacFail v ->
 	if not !just_parsing then begin try
-	  interp v; raise HasNotFailed
+	  (* If the command actually works, ignore its effects on the state *)
+	  States.with_state_protection
+	    (fun v -> interp v; raise HasNotFailed) v
 	with e -> match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")
-- 
cgit v1.2.3