1 files changed, 17 insertions, 10 deletions
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy b/Test/dafny0/Trait/TraitMultiModule.dfy
index f60db7b4..81f4f401 100644
--- a/Test/dafny0/Trait/TraitMultiModule.dfy
+++ b/Test/dafny0/Trait/TraitMultiModule.dfy
@@ -5,22 +5,29 @@ module M1
 {
   trait T1
   {
-     method M1 (a:int)    
+    method M1 (a:int)    
   }
   class C1 extends T1
   {
-     method M1 (x:int)
-     {
-        var y: int := x;
-     }
+    method M1 (x:int)
+    {
+      var y: int := x;
+    }
   }
 }
 
 module M2
 {
-   class C2 extends T1
-   {
-   
-   }
+  import opened M1
+  class C2 extends T1  // error: currently no support to implement trait in different module
+  {
+  }
+}
 
-} 
-\ No newline at end of file
+module M3
+{
+  import M1
+  class C2 extends M1.T1  // error: currently no support to implement trait in different module
+  {
+  }
+}