Stop pretty-print from emitting deprecated semi-colons.

8 files changed, 13 insertions, 13 deletions

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))) }