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

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 5f116779..17867100 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -543,13 +543,13 @@ namespace Microsoft.Dafny
       }

 

       if (f is Predicate) {

-        return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

+        return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, formals,

           req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

       } else if (f is CoPredicate) {

-        return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

+        return new CoPredicate(tok, f.Name, f.IsStatic, tps, formals,

           req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

       } else {

-        return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, refinementCloner.CloneType(f.ResultType),

+        return new Function(tok, f.Name, f.IsStatic, isGhost, tps, formals, refinementCloner.CloneType(f.ResultType),

           req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

       }

     }