From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 test-suite/failure/evarclear1.v | 10 ++++++++++
 test-suite/failure/evarclear2.v |  9 +++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 test-suite/failure/evarclear1.v
 create mode 100644 test-suite/failure/evarclear2.v

(limited to 'test-suite/failure')

diff --git a/test-suite/failure/evarclear1.v b/test-suite/failure/evarclear1.v
new file mode 100644
index 00000000..2e9fa0f3
--- /dev/null
+++ b/test-suite/failure/evarclear1.v
@@ -0,0 +1,10 @@
+Set Printing Existential Instances.
+Set Printing All.
+Goal forall y, let z := S y in exists x, x = 0.
+intros.
+eexists.
+unfold z.
+clear y z.
+(* should fail because the evar should no longer be allowed to depend on z *)
+instantiate (1:=z).
+
diff --git a/test-suite/failure/evarclear2.v b/test-suite/failure/evarclear2.v
new file mode 100644
index 00000000..e606a06f
--- /dev/null
+++ b/test-suite/failure/evarclear2.v
@@ -0,0 +1,9 @@
+Set Printing Existential Instances.
+Set Printing All.
+Goal let y:=0 in exists x:y=y, x = x.
+intros.
+eexists.
+rename y into z.
+unfold z at 1 2.
+(* should fail because the evar type depends on z *)
+clear z.
-- 
cgit v1.2.3