aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-08-19 12:25:32 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2013-08-19 12:25:32 -0400
commitf718e640c3cbe6a891519364992117f49ca333fa (patch)
treeb7581cc191267590b2ee407d91161bd2950e3604 /src/elab_print.sml
parent42fab45125992244c499ec5ac64e0376109bd4cb (diff)
Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml22
1 files changed, 11 insertions, 11 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index c32368a9..7ce94c97 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -680,17 +680,17 @@ and p_sgn env (sgn, _) =
string ":",
space,
p_sgn (E.pushStrNamedAs env x n sgn) sgn']
- | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
- space,
- string "where",
- space,
- string "con",
- space,
- string x,
- space,
- string "=",
- space,
- p_con env c]
+ | SgnWhere (sgn, ms, x, c) => box [p_sgn env sgn,
+ space,
+ string "where",
+ space,
+ string "con",
+ space,
+ p_list_sep (string ".") string (ms @ [x]),
+ space,
+ string "=",
+ space,
+ p_con env c]
| SgnProj (m1, ms, x) =>
let
val m1x = #1 (E.lookupStrNamed env m1)