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