summaryrefslogtreecommitdiff
path: root/Test/dafny4/Regression0.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny4/Regression0.dfy.expect')
-rw-r--r--Test/dafny4/Regression0.dfy.expect3
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