diff options
author | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-21 13:54:58 +0000 |
---|---|---|
committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-21 13:54:58 +0000 |
commit | cfa3aa27f1141fe732a473efd0cff794694c63bb (patch) | |
tree | 3904eb887185d18375c6d93e68c314a7c464868c /test-suite/failure | |
parent | dc7f5e8bbd6fb7da277ee89278211105157b2041 (diff) |
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
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/circular_subtyping1.v | 2 | ||||
-rw-r--r-- | test-suite/failure/circular_subtyping2.v | 16 |
2 files changed, 3 insertions, 15 deletions
diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v index cfd91a2eb..0b3a8688e 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 75b27bce9..3bacdc655 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 |