summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny4/Bug125.dfy24
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
-
-}