summaryrefslogtreecommitdiff
path: root/Test/dafny0/snapshots/Snapshots1.v1.dfy
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-08-13 07:24:33 -0700
committerGravatar leino <unknown>2014-08-13 07:24:33 -0700
commit2a6bd63460d27db7fc11f7b99e231f4f587b6a70 (patch)
tree26d89193bc29b6c469eb41a8f88b531e4f7c9513 /Test/dafny0/snapshots/Snapshots1.v1.dfy
parent9f24fd54271e0e70aba494905416f58ff0348c7c (diff)
Re-included lost calls to CheckEqualityTypes_Type
Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate)
Diffstat (limited to 'Test/dafny0/snapshots/Snapshots1.v1.dfy')
-rw-r--r--Test/dafny0/snapshots/Snapshots1.v1.dfy4
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy
index 93ad6068..184ac65d 100644
--- a/Test/dafny0/snapshots/Snapshots1.v1.dfy
+++ b/Test/dafny0/snapshots/Snapshots1.v1.dfy
@@ -5,9 +5,9 @@ method M()
}
method N()
- ensures P;
+ ensures P();
-predicate P
+predicate P()
{
true
}