diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-26 19:00:08 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-26 19:00:08 -0700 |
| commit | dde9e3560e445addc6cbcfc5bfb219b0bc5cc79f (patch) | |
| tree | 52dabcd18599de21360662202a075e6bf42d3905 /Dafny | |
| parent | a0158dd53b6937657b8c4e9cb0ec3864eabbd9f4 (diff) | |
Dafny: fixed bug that had omitted the computation of .DefaultCtor for some inductive datatypes
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Resolver.cs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 8ab946dc..233f5415 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -497,8 +497,10 @@ namespace Microsoft.Dafny { allTypeParameters.PopMarker();
if (dt is IndDatatypeDecl) {
+ var idt = (IndDatatypeDecl)dt;
+ dependencies.AddVertex(idt);
foreach (Formal p in ctor.Formals) {
- AddDatatypeDependencyEdge((IndDatatypeDecl)dt, p.Type, dependencies);
+ AddDatatypeDependencyEdge(idt, p.Type, dependencies);
}
}
}
|