From 237b569dd6539fc1730dbd1dda29f83e24ef8d0c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 17 Jan 2015 20:17:17 +0530
Subject: Univs: proper printing of global and local universe names (only
 printing functions touched in the kernel).

---
 pretyping/termops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/termops.ml')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index eee94f228f..5862a8525d 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -46,7 +46,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
 
 let pr_puniverses p u = 
   if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr u ++ str"*)"
+  else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
 
 let rec pr_constr c = match kind_of_term c with
   | Rel n -> str "#"++int n
-- 
cgit v1.2.3