diff options
| author |  Rustan Leino <unknown> | 2013-02-11 19:50:57 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-02-11 19:50:57 -0800 |
| commit | 2c74f9200db870814ea3dae63484cbe969ec3526 (patch) | |
| tree | 26c83369d254a707b80726f63cf350d593a59737 /Test/dafny2 | |
| parent | e0f4d19e19d3cd09acaaec91bef529fc49d0c378 (diff) | |
Report error if type of a quantified variable cannot be inferred
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 19e0645f..777be464 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -121,7 +121,7 @@ ghost method Lemma_Revacc(xs: List, ys: List) assert concat(revacc(xrest, Cons(x, Nil)), ys)
== revacc(xrest, concat(Cons(x, Nil), ys));
- assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
+ assert forall g: _T0, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
assert revacc(xrest, concat(Cons(x, Nil), ys))
== // the assert lemma just above
|