Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/src/elaborate.sml Sat Nov 08 14:42:52 2008 -0500 +++ b/src/elaborate.sml Sat Nov 08 16:02:59 2008 -0500 @@ -2615,14 +2615,14 @@ | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => let - val ran1 = + val ran2 = if n1 = n2 then - ran1 + ran2 else - subStrInSgn (n1, n2) ran1 + subStrInSgn (n2, n1) ran2 in subSgn (env, denv) dom2 dom1; - subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2 + subSgn (E.pushStrNamedAs env m1 n1 dom2, denv) ran1 ran2 end | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))