2 files changed, 4 insertions, 9 deletions
diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping.v
index e89539523..ceccd4607 100644
--- a/test-suite/failure/circular_subtyping1.v
+++ b/test-suite/failure/circular_subtyping.v
@@ -1,7 +1,10 @@
 (* subtyping verification in presence of  pseudo-circularity*)
 Module Type S. End S.
 Module Type T. Declare Module M:S. End T.
-
 Module N:S. End N.
 Module NN <: T. Module M:=N. End NN.
+
 Fail Module P <: T with Module M:=NN := NN.
+
+Module F (X:S) (Y:T with Module M:=X). End F.
+Fail Module G := F N N.
+\ No newline at end of file
diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v
deleted file mode 100644
index f6de884db..000000000
--- a/test-suite/failure/circular_subtyping2.v
+++ /dev/null
@@ -1,8 +0,0 @@
-(*subtyping verification in presence of  pseudo-circularity at functor application *)
-Module Type S. End S.
-Module Type T. Declare Module M:S. End T.
-Module N:S. End N.
-
-Module F (X:S) (Y:T with Module M:=X). End F.
-
-Fail Module G := F N N.
-\ No newline at end of file