Changed the iterator class hover text back to the iterator name (which is consistent with everything else), not the "iterator" keyword

1 files changed, 1 insertions, 2 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index be48e23a..b659811d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -323,8 +323,7 @@ namespace Microsoft.Dafny
       }

       foreach (var module in prog.Modules) {

         foreach (var iter in ModuleDefinition.AllIteratorDecls(module.TopLevelDecls)) {

-          var tok = iter.IteratorKeywordTok;

-          ReportAdditionalInformation(tok, Printer.IteratorClassToString(iter), tok.val.Length);

+          ReportAdditionalInformation(iter.tok, Printer.IteratorClassToString(iter), iter.Name.Length);

         }

       }

     }