aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3284.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-13 09:38:47 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-13 12:08:33 +0200
commitc272523bb9d89fe55d1636b48728e7938a8230dd (patch)
tree6a9b4eee3169298d9371c76558189c1d0b27a2d4 /test-suite/bugs/closed/3284.v
parent54b1d23e062940263b6868945db808d49d011306 (diff)
Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).
Diffstat (limited to 'test-suite/bugs/closed/3284.v')
-rw-r--r--test-suite/bugs/closed/3284.v17
1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3284.v b/test-suite/bugs/closed/3284.v
new file mode 100644
index 000000000..a942887ee
--- /dev/null
+++ b/test-suite/bugs/closed/3284.v
@@ -0,0 +1,17 @@
+(* Several bugs:
+- wrong env in pose_all_metas_as_evars leading to out of scope instance of evar
+- check that metas posed as evars in pose_all_metas_as_evars were
+ resolved was not done
+*)
+
+Axiom functional_extensionality_dep :
+ forall {A : Type} {B : A -> Type} (f g : forall x : A, B x),
+ (forall x : A, f x = g x) -> f = g.
+
+Goal forall A B C (f g : forall (x : A) (y : B x), C x y), forall x:A, (forall x y, f x y = g x y) -> True.
+Proof.
+ intros A B C f g x H.
+ Fail apply @functional_extensionality_dep in H.
+ Fail apply functional_extensionality_dep in H.
+ specialize (H x).
+ apply functional_extensionality_dep in H.