Mercurial > urweb
diff src/elaborate.sml @ 471:20fab0e96217
Tree demo working (and other assorted regressions fixed)
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 06 Nov 2008 19:43:48 -0500 |
| parents | b393c2fc80f8 |
| children | 6ee1c761818f |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Nov 06 18:49:38 2008 -0500 +++ b/src/elaborate.sml Thu Nov 06 19:43:48 2008 -0500 @@ -2282,9 +2282,15 @@ 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 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