From 2be514ca20e1478b6df02ef2b4c2725c319ac934 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Tue, 2 Feb 2016 12:40:07 -0800
Subject: Mark old "import A as B" syntax as deprecated. The new syntax is
 "import A : B"

---
 Test/irondafny0/Queue.dfyi            | 2 +-
 Test/irondafny0/opened_workaround.dfy | 2 +-
 Test/irondafny0/xrefine1.dfy          | 6 +++---
 Test/irondafny0/xrefine2.dfy          | 6 +++---
 Test/irondafny0/xrefine3.dfy          | 6 +++---
 5 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'Test/irondafny0')

diff --git a/Test/irondafny0/Queue.dfyi b/Test/irondafny0/Queue.dfyi
index 9f7eb534..06f4b29e 100644
--- a/Test/irondafny0/Queue.dfyi
+++ b/Test/irondafny0/Queue.dfyi
@@ -17,6 +17,6 @@ abstract module Queue {
 }
 
 abstract module MainSpec {
-    import Q as Queue
+    import Q : Queue
 }
 
diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
index 7464c346..6d44ccfd 100644
--- a/Test/irondafny0/opened_workaround.dfy
+++ b/Test/irondafny0/opened_workaround.dfy
@@ -17,5 +17,5 @@ abstract module B {
 }
 
 abstract module C {
-    import Bee as B       // Works
+    import Bee : B       // Works
 }
diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy
index 4b085e6b..1b835649 100644
--- a/Test/irondafny0/xrefine1.dfy
+++ b/Test/irondafny0/xrefine1.dfy
@@ -9,7 +9,7 @@ abstract module ProtocolSpec {
 
 abstract module HostSpec {
     type HostT
-    import P as ProtocolSpec
+    import P : ProtocolSpec
 
     function method foo(h:HostT) : P.ProtoT
 }
@@ -42,8 +42,8 @@ module HostImpl exclusively refines HostSpec {
 }
 
 abstract module MainSpec {
-    import HI as HostSpec
-    import PI as ProtocolSpec
+    import HI : HostSpec
+    import PI : ProtocolSpec
 
     method Test(h1:HI.HostT, h2:HI.HostT) 
         requires HI.foo(h1) == HI.foo(h2);
diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy
index 1de4e201..9c33391b 100644
--- a/Test/irondafny0/xrefine2.dfy
+++ b/Test/irondafny0/xrefine2.dfy
@@ -9,7 +9,7 @@ abstract module ProtocolSpec {
 
 abstract module HostSpec {
     type HostT
-    import P as ProtocolSpec
+    import P : ProtocolSpec
 
     function method foo(h:HostT) : P.ProtoT
 }
@@ -42,8 +42,8 @@ module HostImpl exclusively refines HostSpec {
 }
 
 abstract module MainSpec {
-    import HI as HostSpec
-    import PI as ProtocolSpec
+    import HI : HostSpec
+    import PI : ProtocolSpec
 
     method Test(h1:HI.HostT, h2:HI.HostT) 
         requires HI.foo(h1) == HI.foo(h2);
diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy
index 44add7cc..86dbd957 100644
--- a/Test/irondafny0/xrefine3.dfy
+++ b/Test/irondafny0/xrefine3.dfy
@@ -12,7 +12,7 @@ abstract module AlphaSpec {
 
 abstract module BetaSpec {
     type Beta
-    import A as AlphaSpec
+    import A : AlphaSpec
 
     predicate IsValid(b:Beta)
 
@@ -49,8 +49,8 @@ module BetaImpl exclusively refines BetaSpec {
 }
 
 abstract module MainSpec {
-    import A as AlphaSpec
-    import B as BetaSpec
+    import A : AlphaSpec
+    import B : BetaSpec
 
     method Main()
     {
-- 
cgit v1.2.3