From 565b411b3dafa597232f99c018a11163dcda5175 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 27 Aug 2014 15:28:48 -0700
Subject: Disallow parentheses-less declarations of predicates and
 co-predicates, along with a backward-compatibility warning message if such
 declarations are attempted

---
 Test/dafny2/StoreAndRetrieve.dfy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/dafny2')

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 6255ee96..d5a9d901 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -5,7 +5,7 @@ abstract module A {
   import L = Library;
   class {:autocontracts} StoreAndRetrieve<Thing(==)> {
     ghost var Contents: set<Thing>;
-    predicate Valid
+    predicate Valid()
     {
       true
     }
@@ -31,7 +31,7 @@ abstract module A {
 module B refines A {
   class StoreAndRetrieve<Thing(==)> {
     var arr: seq<Thing>;
-    predicate Valid
+    predicate Valid()
     {
       Contents == set x | x in arr
     }
-- 
cgit v1.2.3