From cd206ac033a1e369277f824dd3a13eca32f0396c Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 3 Apr 2014 18:28:56 -0700
Subject: Added "modify" statement. In a frame govered by a ghost context,
 ignore explicit mentions of `g if g is a ghost field.

---
 Util/latex/dafny.sty | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Util/latex')

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 361b72d2..785cf6f1 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -16,7 +16,7 @@
       match,case,false,true,null,old,fresh,this,
       % statements
       assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
-      where,calc
+      where,calc,modify
       },
   literate=%
     {:}{$\colon$}1
-- 
cgit v1.2.3