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

4 files changed, 8 insertions, 8 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;

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 3ffa5a23..3025cc00 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -130,6 +130,6 @@ abstract module Regression {
 

   abstract module B

   {

-    import X as A

+    import X : A

   }

 }

diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy
index a8dde8ce..beb80546 100644
--- a/Test/dafny0/Modules2.dfy
+++ b/Test/dafny0/Modules2.dfy
@@ -31,7 +31,7 @@ module Test {
 }

 

 module Test2 {

-  import opened B as A

+  import opened B : A

   method m() {

     var c := new C;   // fine, as A was opened

     var c' := new B.C;// also fine, as A is bound

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index e1c0756c..b3cde309 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -44,7 +44,7 @@ module A' refines A {
 }

 

 module B {

-  import X as A

+  import X : A

   method Main() {

     var c := new X.C();

     c.M();  // fine

@@ -68,7 +68,7 @@ module B {
   }

 }

 module B_direct {

-  import X as A'

+  import X : A'

   method Main() {

     var c := new X.C();

     c.M();  // fine