diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-06-16 14:38:01 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-06-16 14:38:01 -0400 |
| commit | 4dce690086c8d6132c22d5c47a0561a4b1261293 (patch) | |
| tree | 58dd4551f8c5d971e12e1c704f7abd9d90f3373e /src/elab_env.sml | |
| parent | c23f27988ff76b4923a63ced2452c4fd7787a745 (diff) | |
Fix a bug in type class enrichment from substructures
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 2296d819..c7dfc0b1 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1070,6 +1070,9 @@ and hnormSgn env (all as (sgn, loc)) = end | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" +fun manifest (m, ms, loc) = + foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms + fun enrichClasses env classes (m1, ms) sgn = case #1 (hnormSgn env sgn) of SgnConst sgis => @@ -1089,10 +1092,15 @@ fun enrichClasses env classes (m1, ms) sgn = in case #1 sgi of SgiStr (x, _, sgn) => - (enrichClasses env classes (m1, ms @ [x]) sgn, - newClasses, - sgiSeek (#1 sgi, fmap), - env) + let + val str = manifest (m1, ms, #2 sgi) + val sgn' = sgnSubSgn (str, fmap) sgn + in + (enrichClasses env classes (m1, ms @ [x]) sgn', + newClasses, + sgiSeek (#1 sgi, fmap), + env) + end | SgiSgn (x, n, sgn) => (classes, newClasses, |