diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-06-02 11:50:53 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-06-02 11:50:53 -0400 |
| commit | 0f7b6944108ad94e899c41033eef15917ed1065c (patch) | |
| tree | 4cbf52d1978e57eba75d8fbbb9091394c67d0a6a /src/elaborate.sml | |
| parent | becba29a1753db244749e87ba13eebd1be401ef6 (diff) | |
Do 'open constraints' automatically; fix sourceless <cselect> monoize bug; Monad library module
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 11 |
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) |