diff src/elab_env.sml @ 849:e571fb150a9f

Fix a bug in type class enrichment from substructures
author Adam Chlipala <adamc@hcoop.net>
date Tue, 16 Jun 2009 14:38:01 -0400
parents 7f871c03e3a1
children 6d9538ce94d8
line wrap: on
line diff
--- a/src/elab_env.sml	Sat Jun 13 15:42:24 2009 -0400
+++ b/src/elab_env.sml	Tue Jun 16 14:38:01 2009 -0400
@@ -1070,6 +1070,9 @@
             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 @@
                           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,