From ef4e0c207abd0e41badf7bf0052b498eb6c01d43 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Fri, 7 Feb 2020 10:34:21 -0500
Subject: Fix signature matching of an imported datatype vs. a fresh datatype

---
 src/elab_print.sml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'src/elab_print.sml')

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 "=",
-- 
cgit v1.2.3