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/dafny3/CachedContainer.dfy.expect | 1 +
 Test/dafny3/GenericSort.dfy            | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/CachedContainer.dfy.expect b/Test/dafny3/CachedContainer.dfy.expect
index c6c90498..0185aacd 100644
--- a/Test/dafny3/CachedContainer.dfy.expect
+++ b/Test/dafny3/CachedContainer.dfy.expect
@@ -1,2 +1,3 @@
+CachedContainer.dfy(120,25): Warning: "import A as B" has been deprecated; in the new syntax, it is "import A:B"
 
 Dafny program verifier finished with 47 verified, 0 errors
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index ea75c196..7555817c 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -17,7 +17,7 @@ abstract module TotalOrder {
 }
 
 abstract module Sort {
-  import O as TotalOrder  // let O denote some module that has the members of TotalOrder
+  import O : TotalOrder  // let O denote some module that has the members of TotalOrder
 
   predicate Sorted(a: array<O.T>, low: int, high: int)
     requires a != null && 0 <= low <= high <= a.Length
-- 
cgit v1.2.3