Mercurial > urweb
changeset 65:2adb20eebee3
Proper subsignaturing for sub-signatures
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 26 Jun 2008 09:03:38 -0400 |
parents | d609820c5834 |
children | 1ec5703c09c4 |
files | src/elaborate.sml tests/subs_sig.lac tests/subs_sig.lig |
diffstat | 3 files changed, 24 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Jun 26 08:54:49 2008 -0400 +++ b/src/elaborate.sml Thu Jun 26 09:03:38 2008 -0400 @@ -1353,9 +1353,18 @@ case sgi1 of L'.SgiSgn (x', n1, sgn1) => if x = x' then - (subSgn env sgn1 sgn2; - subSgn env sgn2 sgn1; - SOME env) + let + val () = subSgn env sgn1 sgn2 + val () = subSgn env sgn2 sgn1 + + val env = E.pushSgnNamedAs env x n2 sgn2 + val env = if n1 = n2 then + env + else + E.pushSgnNamedAs env x n1 sgn2 + in + SOME env + end else NONE | _ => NONE)