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.

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) {