Mercurial > urweb
comparison 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 |
comparison
equal
deleted
inserted
replaced
627:f4f2b09a533a | 628:12b73f3c108e |
---|---|
89 p_kind env k, | 89 p_kind env k, |
90 space, | 90 space, |
91 string "->", | 91 string "->", |
92 space, | 92 space, |
93 p_con (E.pushCRel env x k) c]) | 93 p_con (E.pushCRel env x k) c]) |
94 | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1, | 94 | TDisjoint (c1, c2, c3) => parenIf par (box [string "[", |
95 space, | 95 p_con env c1, |
96 string (case ai of | 96 space, |
97 Instantiate => "~" | 97 string "~", |
98 | LeaveAlone => "~~"), | 98 space, |
99 space, | 99 p_con env c2, |
100 p_con env c2, | 100 string "]", |
101 space, | 101 space, |
102 string "=>", | 102 string "=>", |
103 space, | 103 space, |
104 p_con env c3]) | 104 p_con env c3]) |
105 | TRecord (CRecord (_, xcs), _) => box [string "{", | 105 | TRecord (CRecord (_, xcs), _) => box [string "{", |
106 p_list (fn (x, c) => | 106 p_list (fn (x, c) => |
107 box [p_name env x, | 107 box [p_name env x, |
108 space, | 108 space, |
109 string ":", | 109 string ":", |