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/DisplayExpressions.dfy.expect | |
| 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/DisplayExpressions.dfy.expect')
| -rw-r--r-- | Test/dafny0/DisplayExpressions.dfy.expect | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect index 7374db2a..e12353f7 100644 --- a/Test/dafny0/DisplayExpressions.dfy.expect +++ b/Test/dafny0/DisplayExpressions.dfy.expect @@ -1,5 +1,6 @@ -DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an opaque type.
-DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
-DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
-DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an opaque type.
-4 resolution/type errors detected in DisplayExpressions.dfy
+DisplayExpressions.dfy(5,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(10,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(15,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(20,6): Error: the type of this variable is underspecified
+DisplayExpressions.dfy(25,12): Error: the type of this expression is underspecified
+5 resolution/type errors detected in DisplayExpressions.dfy
|