diff src/expl_util.sml @ 1864:1aa9629e3a4c

Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
author Adam Chlipala <adam@chlipala.net>
date Mon, 19 Aug 2013 12:25:32 -0400
parents 0e554bfd6d6a
children
line wrap: on
line diff
--- a/src/expl_util.sml	Sat Aug 10 10:13:40 2013 -0400
+++ b/src/expl_util.sml	Mon Aug 19 12:25:32 2013 -0400
@@ -526,12 +526,12 @@
                             S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
                                     fn s2' =>
                                        (SgnFun (m, n, s1', s2'), loc)))
-              | SgnWhere (sgn, x, c) =>
+              | SgnWhere (sgn, ms, x, c) =>
                 S.bind2 (sg ctx sgn,
                       fn sgn' =>
                          S.map2 (con ctx c,
                               fn c' =>
-                                 (SgnWhere (sgn', x, c'), loc)))
+                                 (SgnWhere (sgn', ms, x, c'), loc)))
               | SgnProj _ => S.return2 sAll
     in
         sg