From 8cb6251702b09186ca41c5ce67464b83ccfb3d16 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Jun 2014 11:45:51 +0200
Subject: Fixing "clear" in internal_cut_replace: forbid dependencies in the
 name of replaced hypothesis.

---
 test-suite/bugs/closed/3284.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3284.v b/test-suite/bugs/closed/3284.v
index a942887ee9..34cd09c6f4 100644
--- a/test-suite/bugs/closed/3284.v
+++ b/test-suite/bugs/closed/3284.v
@@ -13,5 +13,11 @@ Proof.
   intros A B C f g x H.
   Fail apply @functional_extensionality_dep in H.
   Fail apply functional_extensionality_dep in H.
+  eapply functional_extensionality_dep in H.
+Abort.
+
+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.
   specialize (H x).
   apply functional_extensionality_dep in H.
-- 
cgit v1.2.3