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) =>