Stop pretty-print from emitting deprecated semi-colons.

4 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
index 24cd541c..f06c8021 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
@@ -35,7 +35,7 @@
 // verifies and compiles the program (for this program in less than 2 seconds)

 // without further human intervention.

 

-datatype Tree = Null | Node(Tree, int, Tree);

+datatype Tree = Null | Node(Tree, int, Tree)

 

 function Contains(t: Tree, v: int): bool

 {

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 4b8c9b4c..8af0afe9 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -4,7 +4,7 @@
 /* Lists */

 // Here are some standard definitions of List and functions on Lists

 

-datatype List<T> = Nil | Cons(T, List);

+datatype List<T> = Nil | Cons(T, List)

 

 function length(l: List): nat

 {

diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy
index 12e86018..d6817ce9 100644
--- a/Test/dafny2/MonotonicHeapstate.dfy
+++ b/Test/dafny2/MonotonicHeapstate.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 module M0 {

-  datatype Kind = Constant | Ident | Binary;

+  datatype Kind = Constant | Ident | Binary

 

   class Expr {

     var kind: Kind;

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index d5a9d901..e39913a8 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 abstract module A {

-  import L = Library;

+  import L = Library

   class {:autocontracts} StoreAndRetrieve<Thing(==)> {

     ghost var Contents: set<Thing>;

     predicate Valid()