diff options
| author |  Rustan Leino <unknown> | 2013-12-19 17:20:04 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-19 17:20:04 -0800 |
| commit | 7d1039a3aaedb0baba6090d318d01dae9217b7aa (patch) | |
| tree | e1bb6fc9c7795680c3df397b0c6188305ae7fbeb /Source/DafnyExtension | |
| parent | 72dba23b3ec67244cdf7c598a953bf4fdf32a001 (diff) | |
Compute default decreases clauses in Resolver instead of in the Translator.
Make this information available as AdditionalInformation, that is, as hover text in the IDE.
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index ad2bea8b..246ad645 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -169,7 +169,7 @@ namespace DafnyLanguage iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, module));
iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, module));
iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, module));
- if (!iter.InferredDecreases) {
+ if (!((ICallable)iter).InferredDecreases) {
iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
}
if (iter.Body != null) {
|