Stop pretty-print from emitting deprecated semi-colons.

1 files changed, 10 insertions, 10 deletions

diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect
index aceb685a..1e6a4f11 100644
--- a/Test/dafny0/Simple.dfy.expect
+++ b/Test/dafny0/Simple.dfy.expect
@@ -1,18 +1,18 @@
 // Simple.dfy

 

 class MyClass<T, U> {

-  var x: int;

+  var x: int

 

   method M(s: bool, lotsaObjects: set<object>)

       returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)

-    requires s;

-    modifies this, lotsaObjects;

-    ensures t == t;

-    ensures old(null) != this;

+    requires s

+    modifies this, lotsaObjects

+    ensures t == t

+    ensures old(null) != this

   {

     x := 12;

     while x < 100

-      invariant x <= 100;

+      invariant x <= 100

     {

       x := x + 17;

       if x % 20 == 3 {

@@ -49,17 +49,17 @@ datatype List<T> = Nil | Cons(T, List<T>)
 datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)

 

 class C {

-  var w: WildData;

-  var list: List<bool>;

+  var w: WildData

+  var list: List<bool>

 }

 

 lemma M(x: int)

-  ensures x < 8;

+  ensures x < 8

 {

 }

 

 colemma M'(x': int)

-  ensures true;

+  ensures true

 {

 }