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

0 files changed, 0 insertions, 0 deletions