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