Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 965f0787..7a443e47 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -109,8 +109,8 @@ module T refines S {
   }

 }

 module A {

-   import X as S default T

-   import Y as S default T

+   import X : T

+   import Y : T

    import Z = T

    method run() {

      var x := new X.C;

@@ -128,7 +128,7 @@ method NotMain() {
 

 

 abstract module S1 {

-  import B as S default T

+  import B : T

   method do()

 }

 

@@ -138,7 +138,7 @@ module T1 refines S1 {
   }

 }

 module A1 {

-   import X as S1 default T1

+   import X : T1

    method run() {

      X.do();

      var x := new X.B.C;