Mercurial > urweb
comparison src/elaborate.sml @ 792:d20d6afc1206
Improvements while working on Graftid
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 12 May 2009 18:02:25 -0400 |
parents | 87a7702d681d |
children | 9330ba3a2799 |
comparison
equal
deleted
inserted
replaced
791:5368deb3764b | 792:d20d6afc1206 |
---|---|
1169 default () | 1169 default () |
1170 end | 1170 end |
1171 | (L'.TDisjoint (r1, r2, t'), loc) => | 1171 | (L'.TDisjoint (r1, r2, t'), loc) => |
1172 if infer <> L.TypesOnly then | 1172 if infer <> L.TypesOnly then |
1173 let | 1173 let |
1174 val gs = D.prove env denv (r1, r2, loc) | 1174 val gs = D.prove env denv (r1, r2, #2 e) |
1175 val (e, t, gs') = unravel (t', e) | 1175 val (e, t, gs') = unravel (t', e) |
1176 in | 1176 in |
1177 (e, t, enD gs @ gs') | 1177 (e, t, enD gs @ gs') |
1178 end | 1178 end |
1179 else | 1179 else |