From 85c4b9df59985030127cc8af25395db271952abf Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 17 Sep 2007 12:35:30 +0000
Subject: New files.

---
 etc/coq/lostmessages.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 etc/coq/lostmessages.v

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