From 14c5b4bb8a9c5f62081594d2beaca274eaa0b8f3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Nov 2018 12:55:21 +0100
Subject: Print full binders in subtyping incompatible polymorphism error.

Close #8891
---
 printing/printer.ml  | 13 ++++++++++++-
 printing/printer.mli |  1 +
 2 files changed, 13 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index da364c8b9e..8227933433 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi =
 let pr_global_env = Nametab.pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
+let pr_universe_instance_constraints evd inst csts =
+  let open Univ in
+  let prlev = Termops.pr_evd_level evd in
+  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)
+           (Constraint.elements csts)
+  in
+  str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}"
+
 let pr_universe_instance evd inst =
-  str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+  pr_universe_instance_constraints evd inst Univ.Constraint.empty
 
 let pr_puniverses f env sigma (c,u) =
   if !Constrextern.print_universes
diff --git a/printing/printer.mli b/printing/printer.mli
index f9d1a62895..e50b02b508 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -85,6 +85,7 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
+val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
 val pr_abstract_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
-- 
cgit v1.2.3