comparison src/elab_print.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 bb942416bf1c
children 403f0cc65b9c
comparison
equal deleted inserted replaced
1863:32784d27b5bc 1864:1aa9629e3a4c
678 string ")", 678 string ")",
679 space, 679 space,
680 string ":", 680 string ":",
681 space, 681 space,
682 p_sgn (E.pushStrNamedAs env x n sgn) sgn'] 682 p_sgn (E.pushStrNamedAs env x n sgn) sgn']
683 | SgnWhere (sgn, x, c) => box [p_sgn env sgn, 683 | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
684 space, 684 space,
685 string "where", 685 string "where",
686 space, 686 space,
687 string "con", 687 string "con",
688 space, 688 space,
689 string x, 689 p_list_sep (string ".") string (ms @ [x]),
690 space, 690 space,
691 string "=", 691 string "=",
692 space, 692 space,
693 p_con env c] 693 p_con env c]
694 | SgnProj (m1, ms, x) => 694 | SgnProj (m1, ms, x) =>
695 let 695 let
696 val m1x = #1 (E.lookupStrNamed env m1) 696 val m1x = #1 (E.lookupStrNamed env m1)
697 handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1 697 handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1
698 698