diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-19 15:12:15 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-19 15:12:15 +0000 |
commit | 2c4808858e7d0ce7ef8c679eb060b3567b0a96b5 (patch) | |
tree | e3392ad8106346e4bf08866f65024621a5368683 /test-suite/failure | |
parent | 6af8388fa6257a815c8b385c3b58863263a3a00f (diff) |
Tests de référence circulaire au sous-typage de module (pour mémoire)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9501 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/circular_subtyping1.v | 7 | ||||
-rw-r--r-- | test-suite/failure/circular_subtyping2.v | 20 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v new file mode 100644 index 000000000..cfd91a2eb --- /dev/null +++ b/test-suite/failure/circular_subtyping1.v @@ -0,0 +1,7 @@ +(* Circular substitution check in subtyping verification *) +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. +Module P <: T with Module M:=NN := NN. diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v new file mode 100644 index 000000000..75b27bce9 --- /dev/null +++ b/test-suite/failure/circular_subtyping2.v @@ -0,0 +1,20 @@ +(* Circular substitution check 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. +*) +*) |