summaryrefslogtreecommitdiff
path: root/Test/dafny0/Predicates.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Predicates.dfy')
-rw-r--r--Test/dafny0/Predicates.dfy10
1 files changed, 6 insertions, 4 deletions
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 146129b5..8857482f 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -78,9 +78,10 @@ module Tight refines Loose {
}
}
-module UnawareClient imports Loose {
+module UnawareClient {
+ module L = Loose;
method Main0() {
- var n := new MyNumber.Init();
+ var n := new L.MyNumber.Init();
assert n.N == 0; // error: this is not known
n.Inc();
n.Inc();
@@ -89,9 +90,10 @@ module UnawareClient imports Loose {
}
}
-module AwareClient imports Tight {
+module AwareClient {
+ module T = Tight;
method Main1() {
- var n := new MyNumber.Init();
+ var n := new T.MyNumber.Init();
assert n.N == 0;
n.Inc();
n.Inc();