2 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/failure/evarclear1.v b/test-suite/failure/evarclear1.v
new file mode 100644
index 000000000..2e9fa0f35
--- /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 000000000..e606a06f1
--- /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.