diff options
| author |  rustanleino <unknown> | 2010-05-15 01:01:15 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-15 01:01:15 +0000 |
| commit | 66d171a4e4e27dc958c7926cbf76756c7c6c7b11 (patch) | |
| tree | a88366dc90890cbeeaba082b0e8f28c118d2388b /Util/latex | |
| parent | a660fb79bf527b42e3238b1810143f4fc3f3b827 (diff) | |
Boogie:
* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes
Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
Diffstat (limited to 'Util/latex')
| -rw-r--r-- | Util/latex/boogie.sty | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index 30a18b82..e07d1399 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -34,7 +34,7 @@ procedure,implementation,
requires,modifies,ensures,free,
% expressions
- false,true,null,old,
+ false,true,null,old,then,
% statements
assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
},
|