Stop pretty-print from emitting deprecated semi-colons.

2 files changed, 5 insertions, 5 deletions

diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index 37f3bd68..be7bc25f 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -11,7 +11,7 @@
 // definition, "car" and "cdr" are declared to be destructors for terms

 // constructed by Apply.

 

-datatype Term = S | K | Apply(car: Term, cdr: Term);

+datatype Term = S | K | Apply(car: Term, cdr: Term)

 

 // The problem defines values to be a subset of the terms.  More precisely,

 // a Value is a Term that fits the following grammar:

@@ -40,7 +40,7 @@ function method IsValue(t: Term): bool
 // A context is essentially a term with one missing subterm, a "hole".  It

 // is defined as follows:

 

-datatype Context = Hole | C_term(Context, Term) | value_C(Term/*Value*/, Context);

+datatype Context = Hole | C_term(Context, Term) | value_C(Term/*Value*/, Context)

 

 // The problem seems to suggest that the value_C form requires a value and

 // a context.  To formalize that notion, we define a predicate that checks this

@@ -270,7 +270,7 @@ ghost method Lemma_ContextPossibilities(t: Term)
 // sequence of terms from "t" to "r", each term reducing to its

 // successor in the trace.

 

-datatype Trace = EmptyTrace | ReductionStep(Trace, Term);

+datatype Trace = EmptyTrace | ReductionStep(Trace, Term)

 

 function IsTrace(trace: Trace, t: Term, r: Term): bool

 {

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index 82192e6d..4a45d011 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"

 

 // The tree datatype

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

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

 

 

 // This datatype is used for the result of the build functions.

@@ -11,7 +11,7 @@ datatype Tree = Leaf | Node(Tree, Tree);
 // build_rec, it also has to yield the rest of the sequence,

 // which still needs to be processed. For function build,

 // this part is not used.

-datatype Result = Fail | Res(t: Tree, sOut: seq<int>);

+datatype Result = Fail | Res(t: Tree, sOut: seq<int>)

 

 

 // Function toList converts a tree to a sequence.