Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7

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 000000000..c2926a2b2
--- /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