summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/Compilation.dfy8
-rw-r--r--Test/dafny0/Modules1.dfy2
-rw-r--r--Test/dafny0/Modules2.dfy2
-rw-r--r--Test/dafny0/OpaqueFunctions.dfy4
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