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/printer.ml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 4840577cbf..ebe8e3eebb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -211,16 +211,21 @@ let pr_universe_ctx sigma ?variance c =
   else
     mt()
 
-let pr_abstract_universe_ctx sigma ?variance c =
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+  let open Univ in
+  let priv = Option.default Univ.ContextSet.empty priv in
+  if !Detyping.print_universes && not (Univ.AUContext.is_empty c && Univ.ContextSet.is_empty priv) then
+    let local = if ContextSet.is_empty priv then mt() else
+        str "local: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) priv
+    in
     fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c) ++ v 0 local) c
   else
     mt()
 
-let pr_constant_universes sigma = function
+let pr_constant_universes sigma ~priv = function
   | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
-  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx
+  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
 
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
-- 
cgit v1.2.3


From 828d9447073b06a85421857d7f8b872af6cdfe6b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 16:23:57 +0100
Subject: Fix printing of private universes.

Set Printing Universes.
Set Universe Polymorphism.
Lemma foo : Type.
Proof. exact (forall _ : Type, Type).
Qed.

Print foo.

Before:
(*
foo@{Top.1} =
Type@{Top.2} -> Type@{Top.3}
     : Type@{Top.1}
(* Top.1 |= Prop < Set
            Set < Top.1
            local: {Top.3 Top.2} |= Top.2 < Top.1
                                    Top.3 < Top.1
                                     *)

foo is universe polymorphic
*)

Now:
(* Public universes:
Top.1 |= Set < Top.1
Private universes:
{Top.3 Top.2} |= Top.2 < Top.1
                 Top.3 < Top.1 *)
---
 printing/printer.ml | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index ebe8e3eebb..94b514239a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -143,7 +143,7 @@ let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 let _ = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
 
-let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+let pr_in_comment x = str "(* " ++ x ++ str " *)"
 
 (** Term printers resilient to [Nametab] errors *)
 
@@ -199,27 +199,25 @@ let safe_pr_constr_env = safe_gen pr_constr_env
 
 let pr_universe_ctx_set sigma c =
   if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
   else
     mt()
 
 let pr_universe_ctx sigma ?variance c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
-    fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+    fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c))
   else
     mt()
 
 let pr_abstract_universe_ctx sigma ?variance c ~priv =
   let open Univ in
   let priv = Option.default Univ.ContextSet.empty priv in
-  if !Detyping.print_universes && not (Univ.AUContext.is_empty c && Univ.ContextSet.is_empty priv) then
-    let local = if ContextSet.is_empty priv then mt() else
-        str "local: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) priv
-    in
-    fnl()++pr_in_comment (fun c -> v 0
-      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c) ++ v 0 local) c
+  let has_priv = not (ContextSet.is_empty priv) in
+  if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then
+    let prlev u = Termops.pr_evd_level sigma u in
+    let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in
+    let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in
+    fnl()++pr_in_comment (pub ++ priv)
   else
     mt()
 
@@ -230,16 +228,14 @@ let pr_constant_universes sigma ~priv = function
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
   && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (fun uii -> v 0 
-      (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+    fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi))
   else
     mt()
 
 let pr_abstract_cumulativity_info sigma cumi =
   if !Detyping.print_universes
   && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
-    fnl()++pr_in_comment (fun uii -> v 0
-      (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+    fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi))
   else
     mt()
 
-- 
cgit v1.2.3