Mercurial > urweb
comparison src/elaborate.sml @ 327:3a57f3b3a3f8
Fix bug in subsignature check for con synonyms
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 11 Sep 2008 18:36:20 -0400 |
parents | 950320f33232 |
children | 58f1260f293f |
comparison
equal
deleted
inserted
replaced
326:950320f33232 | 327:3a57f3b3a3f8 |
---|---|
2476 seek (fn sgi1All as (sgi1, _) => | 2476 seek (fn sgi1All as (sgi1, _) => |
2477 let | 2477 let |
2478 fun found (x', n1, k1, c1) = | 2478 fun found (x', n1, k1, c1) = |
2479 if x = x' then | 2479 if x = x' then |
2480 let | 2480 let |
2481 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv) | 2481 fun good () = |
2482 let | |
2483 val env = E.pushCNamedAs env x n2 k2 (SOME c2) | |
2484 val env = if n1 = n2 then | |
2485 env | |
2486 else | |
2487 E.pushCNamedAs env x n1 k1 (SOME c1) | |
2488 in | |
2489 SOME (env, denv) | |
2490 end | |
2482 in | 2491 in |
2483 (case unifyCons (env, denv) c1 c2 of | 2492 (case unifyCons (env, denv) c1 c2 of |
2484 [] => good () | 2493 [] => good () |
2485 | _ => NONE) | 2494 | _ => NONE) |
2486 handle CUnify (c1, c2, err) => | 2495 handle CUnify (c1, c2, err) => |