aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-13 10:17:06 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-13 10:17:06 -0400
commit3316f3c317e587a5fc2ecf38f061a72b48e3b94e (patch)
treefae8c92c195e5f7976352a337017d285e729f859 /src/elab_util.sml
parent7281dbb2fc2a5f50c1049bad629f330e2ff3f7ca (diff)
Remove closure conversion in favor of zany fun with modules, which also replaces 'page'
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 293e53ac..c14b2c60 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -511,7 +511,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
| DFfiStr (x, _, sgn) =>
bind (ctx, Str (x, sgn))
| DConstraint _ => ctx
- | DPage _ => ctx,
+ | DExport _ => ctx,
mfd ctx d)) ctx ds,
fn ds' => (StrConst ds', loc))
| StrVar _ => S.return2 strAll
@@ -572,12 +572,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
S.map2 (mfc ctx c2,
fn c2' =>
(DConstraint (c1', c2'), loc)))
- | DPage (c, e) =>
- S.bind2 (mfc ctx c,
- fn c' =>
- S.map2 (mfe ctx e,
- fn e' =>
- (DPage (c', e'), loc)))
+ | DExport (en, sgn, str) =>
+ S.bind2 (mfsg ctx sgn,
+ fn sgn' =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (DExport (en, sgn', str'), loc)))
in
mfd
end