Last checkin checked in the wrong version of bug125.dfy. The failure part of

the test was moved into test\dafny0\modules0.dfy so that bug125.dfy can be
verified that it was resolved to the correct types.

1 files changed, 0 insertions, 24 deletions

diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy
index 916dd3f8..5dbdea6f 100644
--- a/Test/dafny4/Bug125.dfy
+++ b/Test/dafny4/Bug125.dfy
@@ -56,27 +56,3 @@ module S refines R {
    assert G.f(20); // should be LibA.G.f

   }

 } 

-

-

-module Library {

-

-  class T { }

-

-}

-

- 

-

-module A {

-

-  import opened Library

-	class T {

-	}

-}

-

- 

-

-module B refines A {

-

-  datatype T = MakeT(int)  // illegal for the same reason as above, but Dafny fails to issue an error

-

-}