summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension/IdentifierTagger.cs
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-10-30 17:13:13 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-10-30 17:13:13 -0700
commitb0c51b6fdf1960bbee547959eaf9b0985dee10a9 (patch)
tree61223cc2bed18d7913cac860cd45d966056ff04b /Source/DafnyExtension/IdentifierTagger.cs
parentd4472576ba4f4678f48313e69733254fb1e7017c (diff)
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
Diffstat (limited to 'Source/DafnyExtension/IdentifierTagger.cs')
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs3
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index ace9ae3f..29e451a6 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -133,6 +133,9 @@ namespace DafnyLanguage
List<IdRegion> newRegions = new List<IdRegion>();
foreach (var module in program.Modules) {
+ if (module.IsFacade) {
+ continue;
+ }
foreach (var d in module.TopLevelDecls) {
if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;