diff options
author | leino <unknown> | 2014-10-08 15:47:13 -0700 |
---|---|---|
committer | leino <unknown> | 2014-10-08 15:47:13 -0700 |
commit | 909884fcf5c2ec6af2e68ceae36d72401d542cb3 (patch) | |
tree | 219a88e5417fdcc7d999a34e005e26eb735061f1 /Test/dafny0/Parallel.dfy | |
parent | 8dcec3ddb5269c5e7195a8072d13e8e547b14323 (diff) |
Stricter rules about that types need to be completely resolved.
Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.
Diffstat (limited to 'Test/dafny0/Parallel.dfy')
-rw-r--r-- | Test/dafny0/Parallel.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 9a76777a..d343a84d 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -196,7 +196,7 @@ ghost method DontDoMuch(x: int) }
method OmittedRange() {
- forall (x) { }
+ forall (x: int) { } // a type is still needed for the bound variable
forall (x) {
DontDoMuch(x);
}
|