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

1 files changed, 2 insertions, 2 deletions

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