From 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 11:16:47 -0400
Subject: Printing of @{} instances for polymorphic references in Print and
 About.

---
 printing/printer.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 5f56adbe6f..25a4aa166b 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -84,6 +84,7 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
+val pr_universe_instance   : Univ.universe_context -> std_ppcmds
 val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
-- 
cgit v1.2.3


From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 Oct 2015 12:36:20 -0400
Subject: Univs: local names handling.

Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
---
 printing/printer.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 25a4aa166b..0a44e4f103 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -84,8 +84,8 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
-val pr_universe_instance   : Univ.universe_context -> std_ppcmds
-val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
+val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
-- 
cgit v1.2.3