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/dafny3/CachedContainer.dfy        | 4 ++--
 Test/dafny3/Filter.dfy                 | 4 ++--
 Test/dafny3/InductionVsCoinduction.dfy | 2 +-
 Test/dafny3/Paulson.dfy                | 4 ++--
 Test/dafny3/SimpleCoinduction.dfy      | 4 ++--
 Test/dafny3/SimpleInduction.dfy        | 2 +-
 Test/dafny3/Streams.dfy                | 4 ++--
 Test/dafny3/Zip.dfy                    | 2 +-
 8 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy
index 18c12862..a3824fbf 100644
--- a/Test/dafny3/CachedContainer.dfy
+++ b/Test/dafny3/CachedContainer.dfy
@@ -117,7 +117,7 @@ module M3 refines M2 {
 
 // here a client of the Container
 module Client {
-  import M as M0 default M2;
+  import M as M0 default M2
   method Test() {
     var c := new M.Container();
     c.Add(56);
@@ -134,7 +134,7 @@ module Client {
 }
 
 module CachedClient refines Client {
-  import M = M3;
+  import M = M3
   method Main() {
     Test();
   }
diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 0d9a7231..24c8e94e 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-codatatype Stream<T> = Cons(head: T, tail: Stream);
+codatatype Stream<T> = Cons(head: T, tail: Stream)
 
 function Tail(s: Stream, n: nat): Stream
 {
@@ -53,7 +53,7 @@ lemma Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)
   }
 }
 
-type PredicateHandle;
+type PredicateHandle
 predicate P<T>(x: T, h: PredicateHandle)
 
 copredicate AllP(s: Stream, h: PredicateHandle)
diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 47754036..89fa6cc8 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -3,7 +3,7 @@
 
 // A definition of a co-inductive datatype Stream, whose values are possibly
 // infinite lists.
-codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>);
+codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>)
 
 /*
   A function that returns a stream consisting of all integers upwards of n.
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index 735963a5..c10c4148 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -5,10 +5,10 @@
 // "Mechanizing Coinduction and Corecursion in Higher-order Logic"
 // by Lawrence C. Paulson, 1996.
 
-codatatype LList<T> = Nil | Cons(head: T, tail: LList);
+codatatype LList<T> = Nil | Cons(head: T, tail: LList)
 
 // Simulate function as arguments
-datatype FunctionHandle<T> = FH(T);
+datatype FunctionHandle<T> = FH(T)
 function Apply<T>(f: FunctionHandle<T>, argument: T): T
 
 // Function composition
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index 00e598c3..6b6d0a9d 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -1,8 +1,8 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-codatatype Stream<T> = Cons(head: T, tail: Stream);
-codatatype IList<T> = Nil | ICons(head: T, tail: IList);
+codatatype Stream<T> = Cons(head: T, tail: Stream)
+codatatype IList<T> = Nil | ICons(head: T, tail: IList)
 
 // -----------------------------------------------------------------------
 
diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 29660099..83ea6d14 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -56,7 +56,7 @@ ghost method FibLemma_All()
   to fill these in automatically.
   */
 
-datatype List<T> = Nil | Cons(head: T, tail: List<T>);
+datatype List<T> = Nil | Cons(head: T, tail: List<T>)
 
 function Append<T>(xs: List<T>, ys: List<T>): List<T>
   decreases xs;
diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index c51f30d4..f45df7ae 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -3,7 +3,7 @@
 
 // ----- Stream
 
-codatatype Stream<T> = Nil | Cons(head: T, tail: Stream);
+codatatype Stream<T> = Nil | Cons(head: T, tail: Stream)
 
 function append(M: Stream, N: Stream): Stream
 {
@@ -14,7 +14,7 @@ function append(M: Stream, N: Stream): Stream
 
 // ----- f, g, and maps
 
-type X;
+type X
 
 function f(x: X): X
 function g(x: X): X
diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 9b1d3671..44342970 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -17,7 +17,7 @@ of reasoning with quantifiers in SMT solvers make the explicit calls
 necessary.
 */
 
-codatatype Stream<T> = Cons(hd: T, tl: Stream);
+codatatype Stream<T> = Cons(hd: T, tl: Stream)
 
 function zip(xs: Stream, ys: Stream): Stream
   { Cons(xs.hd, Cons(ys.hd, zip(xs.tl, ys.tl))) }
-- 
cgit v1.2.3