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/CoResolution.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/CoResolution.dfy.expect')
| -rw-r--r-- | Test/dafny0/CoResolution.dfy.expect | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index 196b3faa..9acb5a58 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -20,5 +20,6 @@ CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined
+CoResolution.dfy(202,12): Error: the type of this expression is underspecified
CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined
-23 resolution/type errors detected in CoResolution.dfy
+24 resolution/type errors detected in CoResolution.dfy
|