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).

---
 printing/printer.ml | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 7d5b71f340..3403fb9c3b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -143,17 +143,12 @@ let pr_constr_pattern t =
   let (sigma, env) = get_current_context () in
   pr_constr_pattern_env env sigma t
 
-let pr_sort s = pr_glob_sort (extern_sort s)
+let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
 let _ = Termops.set_print_constr 
   (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t))
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-let pr_univ_cstr (c:Univ.constraints) =
-  if !Detyping.print_universes && not (Univ.Constraint.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_constraints c)) c
-  else
-    mt()
 
 (** Term printers resilient to [Nametab] errors *)
 
@@ -216,7 +211,8 @@ let safe_pr_constr t =
 
 let pr_universe_ctx c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0 (Univ.pr_universe_context c)) c
+    fnl()++pr_in_comment (fun c -> v 0 
+      (Univ.pr_universe_context Universes.pr_with_global_universes c)) c
   else
     mt()
 
@@ -229,7 +225,7 @@ let pr_global = pr_global_env Id.Set.empty
 let pr_puniverses f env (c,u) =
   f env c ++ 
   (if !Constrextern.print_universes then
-    str"(*" ++ Univ.Instance.pr u ++ str"*)"
+    str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
    else mt ())
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
-- 
cgit v1.2.3