Mercurial > urweb
comparison src/elaborate.sml @ 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 |
comparison
equal
deleted
inserted
replaced
64:d609820c5834 | 65:2adb20eebee3 |
---|---|
1351 | L'.SgiSgn (x, n2, sgn2) => | 1351 | L'.SgiSgn (x, n2, sgn2) => |
1352 seek (fn sgi1All as (sgi1, _) => | 1352 seek (fn sgi1All as (sgi1, _) => |
1353 case sgi1 of | 1353 case sgi1 of |
1354 L'.SgiSgn (x', n1, sgn1) => | 1354 L'.SgiSgn (x', n1, sgn1) => |
1355 if x = x' then | 1355 if x = x' then |
1356 (subSgn env sgn1 sgn2; | 1356 let |
1357 subSgn env sgn2 sgn1; | 1357 val () = subSgn env sgn1 sgn2 |
1358 SOME env) | 1358 val () = subSgn env sgn2 sgn1 |
1359 | |
1360 val env = E.pushSgnNamedAs env x n2 sgn2 | |
1361 val env = if n1 = n2 then | |
1362 env | |
1363 else | |
1364 E.pushSgnNamedAs env x n1 sgn2 | |
1365 in | |
1366 SOME env | |
1367 end | |
1359 else | 1368 else |
1360 NONE | 1369 NONE |
1361 | _ => NONE) | 1370 | _ => NONE) |
1362 end | 1371 end |
1363 in | 1372 in |