diff options
| author |  leino <unknown> | 2014-08-26 11:27:39 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-26 11:27:39 -0700 |
| commit | cf01d66976ffd99f423b93949d0f80bba03fe5d7 (patch) | |
| tree | 4255378b08692d3f5ad871c1c87303d127b2e568 /Source/DafnyExtension | |
| parent | f28472da56c5cb38c343bb1e1d8c791fbf22914f (diff) | |
Various resolution fixes and improvements
Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms.
Added IDE tool tips in newtype constraints.
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index beab8303..3bb8f01c 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -213,6 +213,12 @@ namespace DafnyLanguage IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);
}
}
+ } else if (d is NewtypeDecl) {
+ var dd = (NewtypeDecl)d;
+ if (dd.Var != null) {
+ IdRegion.Add(newRegions, dd.Var.tok, dd.Var, true, module);
+ ExprRegions(dd.Constraint, newRegions, module);
+ }
}
}
}
|