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/vstte2012/Combinators.dfy | 6 +++---
 Test/vstte2012/Tree.dfy        | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'Test/vstte2012')

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