From b0c51b6fdf1960bbee547959eaf9b0985dee10a9 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 30 Oct 2012 17:13:13 -0700
Subject: Rename _reverifyPost to $_reverifyPost, so that it doesn't show up in
 BVD Remove some duplicated hover text in DafnyExtension Enable Code Contracts
 in the build

---
 Source/DafnyExtension/ResolverTagger.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/DafnyExtension/ResolverTagger.cs')

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index d1af6878..ca9ed169 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -311,7 +311,7 @@ namespace DafnyLanguage
       Snapshot = snapshot;
     }
     public SnapshotSpan Span() {
-      Contract.Requires(Snapshot != null);  // requires that Snapshot has been filled in
+      Contract.Assume(Snapshot != null);  // requires that Snapshot has been filled in
       var line = Snapshot.GetLineFromLineNumber(Line);
       Contract.Assume(Column <= line.Length);  // this is really a precondition of the constructor + FillInSnapshot
       var length = Math.Min(line.Length - Column, 5);
-- 
cgit v1.2.3