diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-06 19:43:48 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-06 19:43:48 -0500 |
| commit | 50e456effc2cad22d6a61e08887816096c427658 (patch) | |
| tree | 36109508292ec57f01529ab31699ed8837d3f0c8 /src/elaborate.sml | |
| parent | 3af6c283c504e7e85d9e127f64a5eb72abe583ee (diff) | |
Tree demo working (and other assorted regressions fixed)
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index f0beecdd..e84f5307 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2282,9 +2282,15 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = let val env = case #1 h of L'.SgiCon (x, n, k, c) => - E.pushCNamedAs env x n k (SOME c) + if E.checkENamed env n then + env + else + E.pushCNamedAs env x n k (SOME c) | L'.SgiConAbs (x, n, k) => - E.pushCNamedAs env x n k NONE + if E.checkENamed env n then + env + else + E.pushCNamedAs env x n k NONE | _ => env in seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t @@ -2391,12 +2397,12 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun good () = let - val env = E.sgiBinds env sgi2All + val env = E.sgiBinds env sgi1All val env = if n1 = n2 then env else - E.pushCNamedAs env x n1 k' - (SOME (L'.CNamed n2, loc)) + E.pushCNamedAs env x n2 k' + (SOME (L'.CNamed n1, loc)) in SOME (env, denv) end |