diff options
| author |  rustanleino <unknown> | 2011-01-11 21:21:59 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-01-11 21:21:59 +0000 |
| commit | 178088f3280b0353571ac392dfb85b4c1c6a523f (patch) | |
| tree | 7b72e7e3397ed6ac2cb894372b1b830cee64b4e9 | |
| parent | 8478e257809ffedebdc374141b01a1687e0ae5e0 (diff) | |
Dafny: Fixed error in printing an error message. Changed "function method" to "function" in a test case.
| -rw-r--r-- | Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 87ef94d5..c2d1480a 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -2220,7 +2220,7 @@ namespace Microsoft.Dafny { Contract.Assert( ctor != null); // follows from postcondition of TryGetValue
mc.Ctor = ctor;
if (ctor.Formals.Count != mc.Arguments.Count) {
- Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Arguments.Count, ctor.Formals.Count);
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
}
if (memberNamesUsed.ContainsKey(mc.Id)) {
Error(mc.tok, "member {0} appears in more than one case", mc.Id);
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy index 540225a1..fdda243c 100644 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -165,7 +165,7 @@ class LinkedList<T> { }
}
- static function method ReverseSeq(s: seq<T>): seq<T>
+ static function ReverseSeq(s: seq<T>): seq<T>
{
if s == [] then [] else
ReverseSeq(s[1..]) + [s[0]]
|