summaryrefslogtreecommitdiff
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2020-02-07 10:34:21 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2020-02-07 10:34:21 -0500
commitef4e0c207abd0e41badf7bf0052b498eb6c01d43 (patch)
tree0c799af4d4680a9260c8b6209116b4f1d54b2f28 /src/elab_print.sml
parentb0690cc786c858b4a41c7682937bebd53d318f6a (diff)
Fix signature matching of an imported datatype vs. a fresh datatype
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 8a6a651a..637164f4 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -546,7 +546,10 @@ fun p_datatype env (x, n, xs, cons) =
val env = E.pushCNamedAs env x n k NONE
val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
in
- box [string x,
+ box [(if !debug then
+ string (x ^ "_" ^ Int.toString n)
+ else
+ string x),
p_list_sep (box []) (fn x => box [space, string x]) xs,
space,
string "=",