diff options
| author |  leino <unknown> | 2015-09-28 22:47:35 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 22:47:35 -0700 |
| commit | 8a869bcfaeceb6b5a1d01e9b1c0c08b7000a094e (patch) | |
| tree | 0f160456478e2acd1a86ebaed6f5c623d5cfaf2c /Test/dafny4/Regression0.dfy.expect | |
| parent | 9dd401ba24bf795c73a8d66c0890c760de6c8ad5 (diff) | |
Removed specContextOnly parameter from ResolveStatement.
Moved all bounds discovery to resolution pass 1.
Diffstat (limited to 'Test/dafny4/Regression0.dfy.expect')
| -rw-r--r-- | Test/dafny4/Regression0.dfy.expect | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Test/dafny4/Regression0.dfy.expect b/Test/dafny4/Regression0.dfy.expect index 9d1e3019..566b3e3f 100644 --- a/Test/dafny4/Regression0.dfy.expect +++ b/Test/dafny4/Regression0.dfy.expect @@ -1,4 +1,3 @@ Regression0.dfy(7,15): Error: All elements of display must be of the same type (got string, but type of previous elements is int)
-Regression0.dfy(9,28): Error: the type of this variable is underspecified
Regression0.dfy(11,15): Error: second argument to "in" must be a set, multiset, or sequence with elements of type string, or a map with domain string (instead got ?)
-3 resolution/type errors detected in Regression0.dfy
+2 resolution/type errors detected in Regression0.dfy
|