summaryrefslogtreecommitdiff
path: root/Source/Dafny/Printer.cs
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-03-27 13:51:16 -0700
committerGravatar Rustan Leino <unknown>2013-03-27 13:51:16 -0700
commit5296b17758c3e27bf551e9a322323a37983d7abb (patch)
treea7c818eedf1608eec0e59ff73ac3ee8356939751 /Source/Dafny/Printer.cs
parent5f05e3a1c194dcda48115d7b6a1c5777bd2d5287 (diff)
The "choose" statement, hacky and specialized as it was, is now gone. Use the assign-such-that statement instead. For example: x :| x in S;
Diffstat (limited to 'Source/Dafny/Printer.cs')
-rw-r--r--Source/Dafny/Printer.cs2
1 files changed, 0 insertions, 2 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 930af474..2578f0eb 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1167,8 +1167,6 @@ namespace Microsoft.Dafny {
string op;
int opBindingStrength;
switch (e.Op) {
- case UnaryExpr.Opcode.SetChoose:
- op = "choose "; opBindingStrength = 0; break;
case UnaryExpr.Opcode.Not:
op = "!"; opBindingStrength = 0x60; break;
default: