1 files changed, 0 insertions, 57 deletions
diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
deleted file mode 100644
index 2a5b2be7..00000000
--- a/Test/dafny0/Modules2.dfy
+++ /dev/null
@@ -1,57 +0,0 @@
-
-module A {
-  class C {
-    var f: int;
-  }
-  datatype D = E(int) | F(int);
-  static function f(n:nat): nat
-}
-module B {
-  class C {
-    var f: int;
-  }
-  datatype D = E(int) | F(int);
-  static function f(n:nat): nat
-}
-module Test {
-  import opened A; // nice shorthand for import opened A = A; (see below)
-  method m() {
-    var c := new C;   // fine, as A was opened
-    var c' := new A.C;// also fine, as A is bound
-    var i := 43;
-    var d  := E(i);     // these all refer to the same value
-    var d' := A.E(i);
-    var d'':= A.D.E(i);
-    assert d == d' == d'';
-    assert f(3) >= 0; // true because f(x): nat
-    assert A._default.f(3) >= 0;
-  }
-}
-
-module Test2 {
-  import opened B as A;
-  method m() {
-    var c := new C;   // fine, as A was opened
-    var c' := new B.C;// also fine, as A is bound
-    assert B.f(0) >= 0;
-  }
-}
-
-module Test3 {
-  import opened A;
-  import opened B; // everything in B clashes with A
-  method m() {
-    var c := new C;    // bad, ambiguous between A.C and B.C
-    var c' := new A.C; // good: qualified.
-    var i := 43;
-    var d  := E(i);     // bad, as both A and B give a definition of E
-    var d' := D.E(i);   // bad, as D is still itself ambiguous.
-    var d'':= B.D.E(i); // good, just use the B version
-    assert f(3) >= 0;   // bad because A and be both define f statically.
-  }  
-}
-
-module Test4 {
-  import A = A; // good: looks strange, but A is not bound on the RHS of the equality
-  import B; // the same as the above, but for module B
-}
-\ No newline at end of file