From 6a144b5f5a7e85a02465aa25a19c3b5686e062cb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 31 Aug 2008 15:15:41 -0400 Subject: 'eq' type class --- src/elaborate.sml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index 9fa22026..27b3e3fe 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1584,11 +1584,12 @@ fun elabExp (env, denv) (eAll as (e, loc)) = checkKind env t' tk ktype; (t', gs) end - val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e + val (dom, gs2) = normClassConstraint (env, denv) t' + val (e', et, gs3) = elabExp (E.pushERel env x dom, denv) e in ((L'.EAbs (x, t', et, e'), loc), (L'.TFun (t', et), loc), - enD gs1 @ gs2) + enD gs1 @ enD gs2 @ gs3) end | L.ECApp (e, c) => let -- cgit v1.2.3