From f418ecb6a2915a8b8b9fd5598ced5376cbcb75bc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 18 Sep 2010 08:15:29 +0000
Subject: Fixing bugs #2347 (part 2) and #2388: error message printing was done
 too late, in a global environment which was no longer the correct one,
 leading to the failure of error printing (hence an anomaly) in case the
 command modified the state in several steps.

Now, errors raised by vernac commands are processed in the same
(intermediate) state they were raised from, just before rolling back
to the original state.

that modify the state in several
Now, errors raised by vernac commands that modify the state in several
steps (say S1, S2, ..., Sn) are processed in the state they were
produced in (S1, S2, ... Sn-1),

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/2388.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2388.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
new file mode 100644
index 0000000000..c792671193
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -0,0 +1,10 @@
+(* Error message was not printed in the correct environment *)
+
+Fail Parameters (A:Prop) (a:A A).
+
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.                                              
+Fail Program Instance bool_eq_eqdec : EqDec bool eq := 
+   {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
-- 
cgit v1.2.3