From 3d49ce63bd1aa35ef2e8abc9cc359ad6031c21bb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 13 Nov 2018 16:25:23 +0100
Subject: Print universe names in subtyping error instead of Var(x).

---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 8227933433..7ce08ed6bc 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -250,7 +250,7 @@ let pr_universe_instance_constraints evd inst csts =
   let pcsts = if Constraint.is_empty csts then mt()
     else str " |= " ++
          prlist_with_sep (fun () -> str "," ++ spc())
-           (fun (u,d,v) -> prlev u ++ pr_constraint_type d ++ prlev v)
+           (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v))
            (Constraint.elements csts)
   in
   str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}"
-- 
cgit v1.2.3