diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-21 12:06:35 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-21 12:06:35 -0400 |
| commit | a23f12953a60c8f8d663266a9644a08a905b7b36 (patch) | |
| tree | 017e4ed05769d4fff43b3ecfef4cef440d68653a /src/elaborate.sml | |
| parent | cd8ba90217f6ed7efbf4882b4dcd8e199e510fbb (diff) | |
ListShop skeleton
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 035b95f6..9107f29a 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2292,11 +2292,16 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = env else E.pushCNamedAs env x n1 (L'.KType, loc) - (SOME (L'.CNamed n1, loc)) + (SOME (L'.CNamed n2, loc)) in SOME (env, denv) end + val env = E.pushCNamedAs env x n1 k' NONE + val env = if n1 = n2 then + env + else + E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc)) val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 fun xncBad ((x1, _, t1), (x2, _, t2)) = String.compare (x1, x2) <> EQUAL |