summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-04-03 18:28:56 -0700
committerGravatar Rustan Leino <unknown>2014-04-03 18:28:56 -0700
commitcd206ac033a1e369277f824dd3a13eca32f0396c (patch)
tree23f3d5863237de9def3f5c10cb4974dc3191ef14 /Source/DafnyExtension
parent7c64906cd2eb3d0258b29e91bdc861743a05ff42 (diff)
Added "modify" statement.
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
Diffstat (limited to 'Source/DafnyExtension')
-rw-r--r--Source/DafnyExtension/TokenTagger.cs1
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 889da2c0..48f5d1b4 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -291,6 +291,7 @@ namespace DafnyLanguage
case "match":
case "method":
case "modifies":
+ case "modify":
case "module":
case "multiset":
case "nat":