summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-02 11:50:53 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-02 11:50:53 -0400
commit67d67ecae2fdb8708e6207db04880d89d43ba1cb (patch)
tree4cbf52d1978e57eba75d8fbbb9091394c67d0a6a /src/elaborate.sml
parent97570513feb954bc3845f349700f1117fd50ca4b (diff)
Do 'open constraints' automatically; fix sourceless <cselect> monoize bug; Monad library module
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml11
1 files changed, 8 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 62d99bf3..87c1eb27 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3355,6 +3355,10 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
end
val (env', n) = E.pushStrNamed env x sgn'
+ val denv' =
+ case #1 str' of
+ L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
+ | _ => denv
in
case #1 (hnormSgn env sgn') of
L'.SgnFun _ =>
@@ -3363,7 +3367,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
| _ => strError env (FunctorRebind loc))
| _ => ();
- ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
+ ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv', gs' @ gs))
end
| L.DFfiStr (x, sgn) =>
@@ -3721,14 +3725,15 @@ and elabStr (env, denv) (str, loc) =
let
val (dom', gs1) = elabSgn (env, denv) dom
val (env', n) = E.pushStrNamed env m dom'
- val (str', actual, gs2) = elabStr (env', denv) str
+ val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
+ val (str', actual, gs2) = elabStr (env', denv') str
val (formal, gs3) =
case ranO of
NONE => (actual, [])
| SOME ran =>
let
- val (ran', gs) = elabSgn (env', denv) ran
+ val (ran', gs) = elabSgn (env', denv') ran
in
subSgn env' actual ran';
(ran', gs)