1 files changed, 0 insertions, 30 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
deleted file mode 100644
index c2926a2b..00000000
--- a/test-suite/bugs/closed/shouldsucceed/1738.v
+++ /dev/null
@@ -1,30 +0,0 @@
-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