summaryrefslogtreecommitdiff
path: root/Util/latex
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-08-06 18:37:40 -0700
committerGravatar Rustan Leino <unknown>2013-08-06 18:37:40 -0700
commitb06749500528f113ace48fd2fd7d0412c84a9c78 (patch)
tree9b54dfe7c5d412c2f56e0e5bdefe62501ad4d5f2 /Util/latex
parentb40564833ddf8408d446d5b2c0ba376dbea51c68 (diff)
Removed old keyword "choose"
Diffstat (limited to 'Util/latex')
-rw-r--r--Util/latex/dafny.sty2
1 files changed, 1 insertions, 1 deletions
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index d8d4ad96..f282fa7c 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -13,7 +13,7 @@
returns,yields,abstract,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
- match,case,false,true,null,old,fresh,choose,this,
+ match,case,false,true,null,old,fresh,this,
% statements
assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
where,calc