From 95a75639355c20cb39528f4a9b68f3060a659f88 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Jan 2013 18:15:16 +0000
Subject: Fixing bug #2969 (admit failing after Grab Existential Variables due
 to inconsistency in using evar_hyps which is unfiltered and evar_env which is
 filtered).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16175 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/goal.ml                |  2 +-
 test-suite/bugs/closed/2969.v | 25 +++++++++++++++++++++++++
 2 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/2969.v

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1a7e9a9830..a2efc10f02 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -474,7 +474,7 @@ module V82 = struct
   (* Old style hyps primitive *)
   let hyps evars gl =
     let evi = content evars gl in
-    Evd.evar_hyps evi
+    Evd.evar_filtered_hyps evi
 
   (* Access to ".evar_concl" *)
   let concl evars gl =
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
new file mode 100644
index 0000000000..ff75a1f320
--- /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.
-- 
cgit v1.2.3