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.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 18e4902255..f4852b1089 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -825,3 +825,7 @@ let pr_polymorphic b =
     if b then str"Polymorphic " else str"Monomorphic "
   else mt ()
 
+let pr_universe_instance ctx =
+  let inst = Univ.UContext.instance ctx in
+    str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}"
+
-- 
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.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index f4852b1089..202b4f2bc7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -208,10 +208,10 @@ let safe_pr_constr t =
   let (sigma, env) = get_current_context () in
   safe_pr_constr_env env sigma t
 
-let pr_universe_ctx c =
+let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context Universes.pr_with_global_universes c)) c
+      (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c
   else
     mt()
 
@@ -825,7 +825,7 @@ let pr_polymorphic b =
     if b then str"Polymorphic " else str"Monomorphic "
   else mt ()
 
-let pr_universe_instance ctx =
+let pr_universe_instance evd ctx =
   let inst = Univ.UContext.instance ctx in
-    str"@{" ++ Univ.Instance.pr Univ.Level.pr inst ++ str"}"
+    str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
 
-- 
cgit v1.2.3