Stop pretty-print from emitting deprecated semi-colons.

7 files changed, 21 insertions, 21 deletions

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 5dc398f3..28171896 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -156,7 +156,7 @@ class IntegerInduction {
   }

 }

 

-datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);

+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>)

 

 class DatatypeInduction<T> {

   function LeafCount<T>(tree: Tree<T>): int

@@ -192,7 +192,7 @@ class DatatypeInduction<T> {
 // This is a simple example where the induction hypothesis and the

 // case splits are decoupled.

 

-datatype D = Nothing | Something(D);

+datatype D = Nothing | Something(D)

 

 function FooD(n: nat, d: D): int

   ensures 10 <= FooD(n, d);

diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index a52f994b..41adcf50 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -1,8 +1,8 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

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

-datatype Node<X> = Element(X) | Nary(List<X>);

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

+datatype Node<X> = Element(X) | Nary(List<X>)

 

 function FlattenMain<M>(list: List<M>): List<M>

   ensures IsFlat(FlattenMain(list));

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 0f32d529..55701a93 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -3,17 +3,17 @@
 

 // Datatypes

 

-datatype Bool = False | True;

+datatype Bool = False | True

 

-datatype Nat = Zero | Suc(Nat);

+datatype Nat = Zero | Suc(Nat)

 

-datatype List = Nil | Cons(Nat, List);

+datatype List = Nil | Cons(Nat, List)

 

-datatype Pair = Pair(Nat, Nat);

+datatype Pair = Pair(Nat, Nat)

 

-datatype PList = PNil | PCons(Pair, PList);

+datatype PList = PNil | PCons(Pair, PList)

 

-datatype Tree = Leaf | Node(Tree, Nat, Tree);

+datatype Tree = Leaf | Node(Tree, Nat, Tree)

 

 // Boolean functions

 

@@ -285,7 +285,7 @@ function mirror(t: Tree): Tree
 // applying some prescribed function (here, a value of the type)

 // to some argument.

 

-type FunctionValue;

+type FunctionValue

 function Apply(f: FunctionValue, x: Nat): Nat  // this function is left uninterpreted

 

 // The following functions stand for the constant "false" and "true" functions,

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 854af021..3ae1b555 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -17,7 +17,7 @@ abstract module M0 {
     var childrenVisited: nat;

   }

 

-  datatype Path = Empty | Extend(Path, Node);

+  datatype Path = Empty | Extend(Path, Node)

 

   function Reachable(source: Node, sink: Node, S: set<Node>): bool

     requires null !in S;

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index de07fdcc..7a6b051a 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -13,7 +13,7 @@ class Node {
   ghost var pathFromRoot: Path;

 }

 

-datatype Path = Empty | Extend(Path, Node);

+datatype Path = Empty | Extend(Path, Node)

 

 

 class Main {

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 174e71c8..da64d004 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,12 +1,12 @@
 // RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-datatype List = Nil | Cons(Expr, List);

+datatype List = Nil | Cons(Expr, List)

 

 datatype Expr =

   Const(int) |

   Var(int) |

-  Nary(int, List);

+  Nary(int, List)

 

 function Subst(e: Expr, v: int, val: int): Expr

 {

@@ -50,7 +50,7 @@ lemma Lemma(l: List, v: int, val: int)
 datatype Expression =

   Const(int) |

   Var(int) |

-  Nary(int, seq<Expression>);

+  Nary(int, seq<Expression>)

 

 function Substitute(e: Expression, v: int, val: int): Expression

   decreases e;

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index beb1597e..3c836e37 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -3,9 +3,9 @@
 

 // ------------------ generic list, non-generic tree

 

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

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

 

-datatype Tree = Node(int, List<Tree>);

+datatype Tree = Node(int, List<Tree>)

 

 function Inc(t: Tree): Tree

 {

@@ -22,7 +22,7 @@ function ForestInc(forest: List<Tree>): List<Tree>
 

 // ------------------ generic list, generic tree (but GInc defined only for GTree<int>

 

-datatype GTree<T> = Node(T, List<GTree<T>>);

+datatype GTree<T> = Node(T, List<GTree<T>>)

 

 function GInc(t: GTree<int>): GTree<int>

 {

@@ -39,9 +39,9 @@ function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
 

 // ------------------ non-generic structures

 

-datatype TreeList = Nil | Cons(OneTree, TreeList);

+datatype TreeList = Nil | Cons(OneTree, TreeList)

 

-datatype OneTree = Node(int, TreeList);

+datatype OneTree = Node(int, TreeList)

 

 function XInc(t: OneTree): OneTree

 {