diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny4/Bug125.dfy | 24 |
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
-
-}
|