Dafny: fixed some test cases

1 files changed, 7 insertions, 28 deletions

diff --git a/Test/dafny0/ModulesCycle.dfy b/Test/dafny0/ModulesCycle.dfy
index a7f1caa2..15cad8e8 100644
--- a/Test/dafny0/ModulesCycle.dfy
+++ b/Test/dafny0/ModulesCycle.dfy
@@ -1,33 +1,12 @@
-module M {

-  class T { }

-  class U { }

-}

-

-module N {

-}

-

-module U imports N {

-}

-

-module V imports T {  // error: T is not a module

-}

 

-module A imports B, M {

-  class Y { }

+module V {

+  module t = T;  // error: T is not visible (and isn't even a module)

 }

 

-module B imports N, M {

-  class X { }

+module A {

+  module B = C;

 }

 

-module G imports A, M, A, H, B {  // error: cycle in import graph

-}

-

-module H imports A, N, I {

-}

-

-module I imports J {

-}

-

-module J imports G, M {

-}

+module C {

+  module D = A;

+}
\ No newline at end of file