diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-09-07 10:13:02 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-09-07 10:13:02 -0400 |
| commit | 79c2e18d5d237d48f0803bb874d72b4354ba9b25 (patch) | |
| tree | 3766580321bca3f077b2115ec5cbcd30dd9312a4 /src/elaborate.sml | |
| parent | 700a48cc6e78f75166b6e322207a29981782c4e3 (diff) | |
intToString
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 5770fe5b..bf6137b5 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1923,6 +1923,10 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = val nxs = length xs - 1 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs + val (env', denv') = foldl (fn (x, (env', denv')) => + (E.pushCRel env' x k, + D.enter denv')) (env, denv) xs + val (xcs, (used, env, gs)) = ListUtil.foldlMap (fn ((x, to), (used, env, gs)) => @@ -1931,9 +1935,9 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = NONE => (NONE, t, gs) | SOME t' => let - val (t', tk, gs') = elabCon (env, denv) t' + val (t', tk, gs') = elabCon (env', denv') t' in - checkKind env t' tk k; + checkKind env' t' tk k; (SOME t', (L'.TFun (t', t), loc), gs' @ gs) end val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs |