Stop pretty-print from emitting deprecated semi-colons.

1 files changed, 6 insertions, 6 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 01c2a0a5..b44f4d68 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -16,26 +16,26 @@ class C {
   }

 }

 

-datatype D = A;

+datatype D = A

 

-datatype NeverendingList = Cons(int, NeverendingList);  // error: no grounding constructor

+datatype NeverendingList = Cons(int, NeverendingList)  // error: no grounding constructor

 

 datatype MutuallyRecursiveDataType<T> =

   FromANumber(int) |  // this is the base case

-  Else(TheCounterpart<T>, C);

+  Else(TheCounterpart<T>, C)

 

 datatype TheCounterpart<T> =

   TreeLike(TheCounterpart<T>, TheCounterpart<T>) |

-  More(MutuallyRecursiveDataType<T>);

+  More(MutuallyRecursiveDataType<T>)

 

 // these 'ReverseOrder_' order tests may be called white-box unit tests

 datatype ReverseOrder_MutuallyRecursiveDataType<T> =

   FromANumber(int) |  // this is the base case

-  Else(ReverseOrder_TheCounterpart<T>, C);

+  Else(ReverseOrder_TheCounterpart<T>, C)

 

 datatype ReverseOrder_TheCounterpart<T> =

   TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |

-  More(ReverseOrder_MutuallyRecursiveDataType<T>);

+  More(ReverseOrder_MutuallyRecursiveDataType<T>)

 

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