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

1 files changed, 1 insertions, 5 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 2ec40e08..56722543 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -438,11 +438,7 @@ namespace Microsoft.Dafny {
       if (f.SignatureIsOmitted) {

         wr.WriteLine(" ...");

       } else {

-        if (f.OpenParen != null) {

-          PrintFormals(f.Formals, f.Name);

-        } else {

-          Contract.Assert(isPredicate);

-        }

+        PrintFormals(f.Formals, f.Name);

         if (!isPredicate) {

           wr.Write(": ");

           PrintType(f.ResultType);