diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-07-09 22:12:23 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-07-09 22:12:23 -0700 |
| commit | 9c332a2e3580d05b1557fa4548901d8df4b423a1 (patch) | |
| tree | 74ab8075f78680943a6ed2762e97261c95d6cd3e /Dafny/Resolver.cs | |
| parent | 3cfc61ac1212e28136a10f35ac1b1e8de743e7d2 (diff) | |
Dafny: More work on the coinduction principle
Diffstat (limited to 'Dafny/Resolver.cs')
| -rw-r--r-- | Dafny/Resolver.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 325745f0..403a7352 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -451,7 +451,7 @@ namespace Microsoft.Dafny { if (members.ContainsKey(formal.Name)) {
Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
} else {
- dtor = new DatatypeDestructor(formal.tok, ctor, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
+ dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
dtor.EnclosingClass = dt; // resolve here
members.Add(formal.Name, dtor);
}
|