Imported Upstream version 8.5~beta1+dfsg

1 files changed, 30 insertions, 0 deletions

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