summaryrefslogtreecommitdiff
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 12:25:12 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 12:25:12 -0400
commitf7d2bdce780d0333431829a8a788bdb208c0dcbc (patch)
tree5316084519f313741563c016ac6733d03f892475 /src/elab_print.sml
parent7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (diff)
Disjointness assumptions in expressions
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 05d216ca..c90a0494 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -77,6 +77,15 @@ fun p_con' par env (c, _) =
string "->",
space,
p_con (E.pushCRel env x k) c])
+ | TDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
+ space,
+ string "~",
+ space,
+ p_con env c2,
+ space,
+ string "->",
+ space,
+ p_con env c3])
| TRecord (CRecord (_, xcs), _) => box [string "{",
p_list (fn (x, c) =>
box [p_name env x,