From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/1738.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test-suite/bugs/closed/1738.v (limited to 'test-suite/bugs/closed/1738.v') diff --git a/test-suite/bugs/closed/1738.v b/test-suite/bugs/closed/1738.v new file mode 100644 index 00000000..c2926a2b --- /dev/null +++ b/test-suite/bugs/closed/1738.v @@ -0,0 +1,30 @@ +Require Import FSets. + +Module SomeSetoids (Import M:FSetInterface.S). + +Lemma Equal_refl : forall s, s[=]s. +Proof. red; split; auto. Qed. + +Add Relation t Equal + reflexivity proved by Equal_refl + symmetry proved by eq_sym + transitivity proved by eq_trans + as EqualSetoid. + +Add Morphism Empty with signature Equal ==> iff as Empty_m. +Proof. +unfold Equal, Empty; firstorder. +Qed. + +End SomeSetoids. + +Module Test (Import M:FSetInterface.S). + Module A:=SomeSetoids M. + Module B:=SomeSetoids M. (* lots of warning *) + + Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'. + intros. + rewrite H in H0. + assumption. +Qed. +End Test. \ No newline at end of file -- cgit v1.2.3