From b0bb7bf96406d8695d5ec2377d9ce2b2acba44f0 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 16 Jul 2013 17:22:18 -0700
Subject: Syntactic improvements in two tests.

---
 Test/dafny3/Filter.dfy  | 2 +-
 Test/dafny3/Paulson.dfy | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index d45f4acc..287b4006 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -164,7 +164,7 @@ ghost method Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)
   requires AlwaysAnother(s, h);
   ensures forall x :: In(x, Filter(s, h)) <==> In(x, s) && P(x, h);
 {
-  forall (x)
+  forall x
     ensures In(x, Filter(s, h)) <==> In(x, s) && P(x, h);
   {
     if In(x, Filter(s, h)) {
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index c1721af3..431ff543 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -150,7 +150,7 @@ ghost method Example7<A>(f: FunctionHandle<LList<A>>)
   // Given the definition of h, prove h(f, _) == Iterates(f, _):
   ensures forall M :: h(f, M) == Iterates(f, M);
 {
-  forall (M) {
+  forall M {
     BisimulationLemma(0, f, M);
   }
 }
-- 
cgit v1.2.3