From db30cafd94527e73e969457c9c00e8c67300d7d4 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 5 Mar 2015 12:04:37 -0800
Subject: Stop pretty-print from emitting deprecated semi-colons.

---
 Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy | 2 +-
 Test/dafny2/Calculations.dfy                            | 2 +-
 Test/dafny2/MonotonicHeapstate.dfy                      | 2 +-
 Test/dafny2/StoreAndRetrieve.dfy                        | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/dafny2')

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()
-- 
cgit v1.2.3