From b4a87643ad21c881c3a54c4872e1520164c2ec6d Mon Sep 17 00:00:00 2001
From: Nadia Polikarpova <nadia.polikarpova@gmail.com>
Date: Wed, 19 Sep 2012 19:01:37 +0200
Subject: Allow multiple calc/block statements in a hint. Removed the empty
 calc test from dafny2/Calculations, as it actually belongs in dafny0.

---
 Test/dafny2/Calculations.dfy | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'Test/dafny2')

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index c48f2000..1ddd8603 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -209,10 +209,4 @@ ghost method Window(xs: List, ys: List)
     length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
     true;
   }
-}
-
-// Empty calculations are also allowed, but they don't generate any Boogie code.
-ghost method Empty()
-{
-	calc {}
-}
+}
\ No newline at end of file
-- 
cgit v1.2.3