diff options
author | Rustan Leino <unknown> | 2014-04-03 18:28:56 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2014-04-03 18:28:56 -0700 |
commit | cd206ac033a1e369277f824dd3a13eca32f0396c (patch) | |
tree | 23f3d5863237de9def3f5c10cb4974dc3191ef14 /Util/vim/dafny.vim | |
parent | 7c64906cd2eb3d0258b29e91bdc861743a05ff42 (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 'Util/vim/dafny.vim')
-rw-r--r-- | Util/vim/dafny.vim | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index f533a621..d6e6bac5 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -11,7 +11,7 @@ syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword abstract module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while -syntax keyword dafnyStatement assume assert return yield new print break label where calc +syntax keyword dafnyStatement assume assert return yield new print break label where calc modify syntax keyword dafnyKeyword var ghost returns yields null static this refines include syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant |