summaryrefslogtreecommitdiff
path: root/Test/hofs/Consequence.dfy.expect
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-01-23 16:17:23 -0800
committerGravatar leino <unknown>2015-01-23 16:17:23 -0800
commit227fa997dd25a41c8bfc86d919635b6677df2c5f (patch)
tree4ac05f6efa2a3d51ff46118c61567f3b1f52d120 /Test/hofs/Consequence.dfy.expect
parent97e7528b3cd3e9b9e21b75abf817d6e0ed3b9df7 (diff)
Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy Fixed comparable-types tests
Diffstat (limited to 'Test/hofs/Consequence.dfy.expect')
-rw-r--r--Test/hofs/Consequence.dfy.expect2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/hofs/Consequence.dfy.expect b/Test/hofs/Consequence.dfy.expect
index 069e7767..52595bf9 100644
--- a/Test/hofs/Consequence.dfy.expect
+++ b/Test/hofs/Consequence.dfy.expect
@@ -1,2 +1,2 @@
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 3 verified, 0 errors