diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 19:01:37 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 19:01:37 +0200 |
| commit | b4a87643ad21c881c3a54c4872e1520164c2ec6d (patch) | |
| tree | 0b48084099a76478d2c8e3887b3d0acec98f892c /Test/dafny2 | |
| parent | b929a1c46a1a158b95a0042a81fc8539ab5eae00 (diff) | |
Allow multiple calc/block statements in a hint. Removed the empty calc test from dafny2/Calculations, as it actually belongs in dafny0.
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 8 |
1 files changed, 1 insertions, 7 deletions
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 |