From cfa3aa27f1141fe732a473efd0cff794694c63bb Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 21 Feb 2007 13:54:58 +0000
Subject: Fixed the pseudo-cicularity problem due to the with operator on
 Module Type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9662 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/failure/circular_subtyping1.v |  2 +-
 test-suite/failure/circular_subtyping2.v | 16 ++--------------
 2 files changed, 3 insertions(+), 15 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v
index cfd91a2eb4..0b3a8688e0 100644
--- a/test-suite/failure/circular_subtyping1.v
+++ b/test-suite/failure/circular_subtyping1.v
@@ -1,4 +1,4 @@
-(* Circular substitution check in subtyping verification *)
+(* subtyping verification in presence of  pseudo-circularity*)
 Module Type S. End S.
 Module Type T. Declare Module M:S. End T.
 
diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v
index 75b27bce97..3bacdc6553 100644
--- a/test-suite/failure/circular_subtyping2.v
+++ b/test-suite/failure/circular_subtyping2.v
@@ -1,20 +1,8 @@
-(* Circular substitution check at functor application *)
+(*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.
-Module A := F N N.
 
-(* Circular substitution check at with definition *)
-(* Should it be implemented?? *)
-(*
-
-Module NN:T. Module M:=N. End NN.
-Module Type U := T with Module M:=NN.
-(*
-User error: The construction "with Module M:=..." is about to create
-a circular module type. Their resolution is not implemented yet.
-If you really need that feature, please report.
-*)
-*)
+Module G := F N N.
\ No newline at end of file
-- 
cgit v1.2.3