1 files changed, 13 insertions, 0 deletions
diff --git a/etc/coq/lostmessages.v b/etc/coq/lostmessages.v
new file mode 100644
index 00000000..d82ddb41
--- /dev/null
+++ b/etc/coq/lostmessages.v
@@ -0,0 +1,13 @@
+(* These are some examples which generate goals and errors at the same
+   moment.  May be broken in development version of Coq.
+   
+   See  http://proofgeneral.inf.ed.ac.uk/trac/ticket/141 
+*)
+
+Require Import Setoid. 
+Goal False. 
+setoid_replace False with True.
+
+Goal True /\ True -> True. 
+intro H. 
+destruct H as [H1 H2 H3].