Disallow parentheses-less declarations of predicates and co-predicates, along with a backward-compatibility warning message if such declarations are attempted

1 files changed, 2 insertions, 2 deletions

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

     }