From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 29 Oct 2018 17:56:10 +0100
Subject: Local universes for opaque polymorphic constants.

---
 printing/prettyp.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 712eb21ee6..f9f4d7f7f8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -96,8 +96,9 @@ let print_ref reduce ref udecl =
     then Printer.pr_universe_instance sigma inst
     else mt ()
   in
+  let priv = None in (* We deliberately don't print private univs in About. *)
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-           Printer.pr_abstract_universe_ctx sigma ?variance univs)
+           Printer.pr_abstract_universe_ctx sigma ?variance univs ~priv)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -580,11 +581,11 @@ let print_constant with_values sep sp udecl =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-        Printer.pr_constant_universes sigma univs
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs
     | Some (c, ctx) ->
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_constant_universes sigma univs)
+        Printer.pr_constant_universes sigma univs ~priv:cb.const_private_poly_univs)
 
 let gallina_print_constant_with_infos sp udecl =
   print_constant true " = " sp udecl ++
-- 
cgit v1.2.3