diff src/elab_print.sml @ 628:12b73f3c108e

Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 354800878b4d
children 70cbdcf5989b
line wrap: on
line diff
--- a/src/elab_print.sml	Sun Feb 22 17:39:55 2009 -0500
+++ b/src/elab_print.sml	Tue Feb 24 12:01:24 2009 -0500
@@ -91,17 +91,17 @@
                                                 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,