summaryrefslogtreecommitdiff
path: root/Test/dafny0/TypeParameters.dfy
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2009-11-05 02:28:36 +0000
committerGravatar rustanleino <unknown>2009-11-05 02:28:36 +0000
commit88c490d4c929ab2815c6a33d9ba604057bdd06a0 (patch)
treed07564e6f7f29ae630097bb68dcc7655ab268709 /Test/dafny0/TypeParameters.dfy
parent48a417d2201f5e4151b1575d4ec011343c69e389 (diff)
The Dafny call statement now automatically declares left-hand sides as local variables, if they were not already local variables.
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
-rw-r--r--Test/dafny0/TypeParameters.dfy1
1 files changed, 0 insertions, 1 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a5764be5..3f57f369 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -13,7 +13,6 @@ class C<U> {
method Main(u: U)
{
var t := F(3,u) && F(this,u);
- var kz;
call kz := M(t,u);
assert kz && (G() || !G());
}