Mercurial > urweb
comparison src/elaborate.sml @ 480:40c737913075
Especialize handles records better
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 08 Nov 2008 16:02:59 -0500 |
parents | 6ee1c761818f |
children | ae03d09043c1 |
comparison
equal
deleted
inserted
replaced
479:ffa18975e661 | 480:40c737913075 |
---|---|
2613 ignore (foldl folder (env, denv) sgis2) | 2613 ignore (foldl folder (env, denv) sgis2) |
2614 end | 2614 end |
2615 | 2615 |
2616 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => | 2616 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => |
2617 let | 2617 let |
2618 val ran1 = | 2618 val ran2 = |
2619 if n1 = n2 then | 2619 if n1 = n2 then |
2620 ran1 | 2620 ran2 |
2621 else | 2621 else |
2622 subStrInSgn (n1, n2) ran1 | 2622 subStrInSgn (n2, n1) ran2 |
2623 in | 2623 in |
2624 subSgn (env, denv) dom2 dom1; | 2624 subSgn (env, denv) dom2 dom1; |
2625 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2 | 2625 subSgn (E.pushStrNamedAs env m1 n1 dom2, denv) ran1 ran2 |
2626 end | 2626 end |
2627 | 2627 |
2628 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) | 2628 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) |
2629 | 2629 |
2630 | 2630 |