comparison 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
comparison
equal deleted inserted replaced
1863:32784d27b5bc 1864:1aa9629e3a4c
524 S.bind2 (sg ctx s1, 524 S.bind2 (sg ctx s1,
525 fn s1' => 525 fn s1' =>
526 S.map2 (sg (bind (ctx, Str (m, s1'))) s2, 526 S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
527 fn s2' => 527 fn s2' =>
528 (SgnFun (m, n, s1', s2'), loc))) 528 (SgnFun (m, n, s1', s2'), loc)))
529 | SgnWhere (sgn, x, c) => 529 | SgnWhere (sgn, ms, x, c) =>
530 S.bind2 (sg ctx sgn, 530 S.bind2 (sg ctx sgn,
531 fn sgn' => 531 fn sgn' =>
532 S.map2 (con ctx c, 532 S.map2 (con ctx c,
533 fn c' => 533 fn c' =>
534 (SgnWhere (sgn', x, c'), loc))) 534 (SgnWhere (sgn', ms, x, c'), loc)))
535 | SgnProj _ => S.return2 sAll 535 | SgnProj _ => S.return2 sAll
536 in 536 in
537 sg 537 sg
538 end 538 end
539 539