Dafny: allow "_" as don't-care variable name

1 files changed, 2 insertions, 2 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 7aaf8944..c2362a72 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -294,7 +294,7 @@ namespace DafnyLanguage
         Contract.Requires(tok != null);

         Contract.Requires(v != null);

         Start = tok.pos;

-        Length = v.Name.Length;

+        Length = v.DisplayName.Length;

         string kind;

         if (v is VarDecl) {

           kind = "local variable";

@@ -304,7 +304,7 @@ namespace DafnyLanguage
           var formal = (Formal)v;

           kind = formal.InParam ? "in-parameter" : "out-parameter";

         }

-        HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);

+        HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);

         IsDefinition = isDefinition;

       }

       private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {