1 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
new file mode 100644
index 00000000..ff75a1f3
--- /dev/null
+++ b/test-suite/bugs/closed/2969.v
@@ -0,0 +1,25 @@
+(* Check that Goal.V82.byps and Goal.V82.env are consistent *)
+
+(* This is a shorten variant of the initial bug which raised anomaly *)
+
+Goal forall x : nat, (forall z, (exists y:nat, z = y) -> True) -> True.
+evar nat.
+intros x H.
+apply (H n).
+unfold n. clear n.
+eexists.
+reflexivity.
+Grab Existential Variables.
+admit.
+
+(* Alternative variant which failed but without raising anomaly *)
+
+Goal forall x : nat, True.
+evar nat.
+intro x.
+evar nat.
+assert (H := eq_refl : n0 = n).
+clearbody n n0.
+exact I.
+Grab Existential Variables.
+admit.