summaryrefslogtreecommitdiff
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 10:55:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 10:55:38 -0400
commit43116f69ce9330eb09d42a25d4afc746e7c3f3ef (patch)
treee57ed0ff271cf35d5dbf88ecb90ce150a877e454 /src/elab_print.sml
parentcc2b6499cd2ea61f8882419cc5915c3428d5f5b7 (diff)
Initial disjointness prover
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 8c51be11..01472ca7 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -48,6 +48,7 @@ fun p_kind' par (k, _) =
p_kind k2])
| KName => string "Name"
| KRecord k => box [string "{", p_kind k, string "}"]
+ | KUnit => string "Unit"
| KError => string "<ERROR>"
| KUnif (_, _, ref (SOME k)) => p_kind' par k
@@ -155,6 +156,8 @@ fun p_con' par env (c, _) =
p_con env c2])
| CFold _ => string "fold"
+ | CUnit => string "()"
+
| CError => string "<ERROR>"
| CUnif (_, _, _, ref (SOME c)) => p_con' par env c
| CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),