From a23f12953a60c8f8d663266a9644a08a905b7b36 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 21 Oct 2008 12:06:35 -0400 Subject: ListShop skeleton --- src/elaborate.sml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src/elaborate.sml') 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 -- cgit v1.2.3