aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 12:01:24 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 12:01:24 -0500
commit7865cb372d95c42542d59cbcf83ba541b0ab3f8a (patch)
tree9dd05f2dad9cc6d4e0e33af1e8f1cf0a1def9f15 /src/elab_print.sml
parentadcf93304e6fc100d0e714a898033d2a9033173c (diff)
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml22
1 files changed, 11 insertions, 11 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index e5dda58e..64d8cfab 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -91,17 +91,17 @@ fun p_con' par env (c, _) =
string "->",
space,
p_con (E.pushCRel env x k) c])
- | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1,
- space,
- string (case ai of
- Instantiate => "~"
- | LeaveAlone => "~~"),
- space,
- p_con env c2,
- space,
- string "=>",
- space,
- p_con env c3])
+ | TDisjoint (c1, c2, c3) => parenIf par (box [string "[",
+ p_con env c1,
+ space,
+ string "~",
+ space,
+ p_con env c2,
+ string "]",
+ space,
+ string "=>",
+ space,
+ p_con env c3])
| TRecord (CRecord (_, xcs), _) => box [string "{",
p_list (fn (x, c) =>
box [p_name env x,