diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 18:56:25 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 18:56:25 -0700 |
| commit | 0a76a9953bd35663e20cc197ae5247a25cadc4bd (patch) | |
| tree | f90a2f242899adc3e98e324fc25451f7e1a79468 /Source/DafnyExtension/IdentifierTagger.cs | |
| parent | 5441447b52d9850683679c1dc7aa675d8ddc2927 (diff) | |
More free antecedents when proving well-formedness of iterator specs
Diffstat (limited to 'Source/DafnyExtension/IdentifierTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index 5ecc8dc2..6577113e 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -173,6 +173,8 @@ namespace DafnyLanguage if (m.Body != null) {
StatementRegions(m.Body, newRegions, module);
}
+ } else if (member is SpecialField) {
+ // do nothing
} else if (member is Field) {
var fld = (Field)member;
IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);
|