Mercurial > urweb

diff src/elab_util.sml @ 1864:1aa9629e3a4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 bb942416bf1c
children 403f0cc65b9c
line wrap: on
line diff
--- a/src/elab_util.sml	Sat Aug 10 10:13:40 2013 -0400
+++ b/src/elab_util.sml	Mon Aug 19 12:25:32 2013 -0400
@@ -759,12 +759,12 @@
                                     fn s2' =>
                                        (SgnFun (m, n, s1', s2'), loc)))
               | SgnProj _ => S.return2 sAll
-              | 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)))
               | SgnError => S.return2 sAll
     in
         sg
@@ -1248,7 +1248,7 @@
         SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
       | SgnVar n => n
       | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
-      | SgnWhere (sgn, _, _) => maxNameSgn sgn
+      | SgnWhere (sgn, _, _, _) => maxNameSgn sgn
       | SgnProj (n, _, _) => n
       | SgnError => 0