Dafny: allow constructors only inside classes, removed semi-colons at end of body-less functions/methods

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a3698dc0..8f3f8b87 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -17,7 +17,7 @@ class C<U> {
     assert kz && (G() || !G());

   }

 

-  function G<Y>(): Y;

+  function G<Y>(): Y

 }

 

 class SetTest {

@@ -99,7 +99,7 @@ class CClient {
 

 // -------------------------

 

-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;

+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool

   requires c == c || c in people;

 

 method FindCelebrity3(people: set<int>, ghost c: int)

@@ -110,7 +110,7 @@ method FindCelebrity3(people: set<int>, ghost c: int)
   b := F(c, people);

 }

 

-static function F(c: int, people: set<int>): bool;

+static function F(c: int, people: set<int>): bool

   requires IsCelebrity(c, people);

 

 function RogerThat<G>(g: G): G

@@ -153,8 +153,8 @@ method LoopyRoger(n: int)
 

 class TyKn_C<T> {

   var x: T;

-  function G(): T;

-  method M() returns (t: T);

+  function G(): T

+  method M() returns (t: T)

 }

 

 class TyKn_K {