summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 12:06:35 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 12:06:35 -0400
commita23f12953a60c8f8d663266a9644a08a905b7b36 (patch)
tree017e4ed05769d4fff43b3ecfef4cef440d68653a /src/elaborate.sml
parentcd8ba90217f6ed7efbf4882b4dcd8e199e510fbb (diff)
ListShop skeleton
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml7
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