From f361ba32a28796514b8d3469c7bee3f43ad61fc1 Mon Sep 17 00:00:00 2001 From: xclerc Date: Fri, 20 Sep 2013 12:57:59 +0000 Subject: Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/failure/circular_subtyping.v | 10 ++++++++++ test-suite/failure/circular_subtyping1.v | 7 ------- test-suite/failure/circular_subtyping2.v | 8 -------- 3 files changed, 10 insertions(+), 15 deletions(-) create mode 100644 test-suite/failure/circular_subtyping.v delete mode 100644 test-suite/failure/circular_subtyping1.v delete mode 100644 test-suite/failure/circular_subtyping2.v (limited to 'test-suite/failure') diff --git a/test-suite/failure/circular_subtyping.v b/test-suite/failure/circular_subtyping.v new file mode 100644 index 000000000..ceccd4607 --- /dev/null +++ b/test-suite/failure/circular_subtyping.v @@ -0,0 +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_subtyping1.v b/test-suite/failure/circular_subtyping1.v deleted file mode 100644 index e89539523..000000000 --- a/test-suite/failure/circular_subtyping1.v +++ /dev/null @@ -1,7 +0,0 @@ -(* 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. 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 -- cgit v1.2.3