[Print Universes] should show current universe constraints, not constraints prior to definition (polyproj)

[JasonGross]

Monomorphic Definition U1 := Type.
Monomorphic Definition U2 := Type.

Set Printing Universes.
Monomorphic Definition foo : True.
pose ((U1 : U2)).
Print Universes. (* Prop < Set *)
Fail pose (U2 : U1).
 (* The command has indeed failed with message:
=> Error:
In environment
u := (U1:U2) : U2
The term "U2" has type "Type (* Top.2+1 *)" while it is expected to have type
 "U1" (Universe inconsistency: Cannot enforce Top.2 < Top.1 because Top.1
< Top.2)).
 *)
exact I.
Defined.
Print Universes.
(* Top.1 < Top.2
Prop < Set *)

I want to see Top.1 < Top.2 in the first case.

[JasonGross]

I bet this is because you don't know at tactic time whether the current definition is monomorphic or polymorphic, and in the polymorphic case, you don't add them to the global graph. So I think either I want the current ones to be shown by Print Universes with some kind of (local) annotation, or I want a separate Print Current Universes or Print Local Universes or something which shows me the ones introduced by the current goal. Alternatively (perhaps my most preferred option), Show Proof should include such a universe graph when Set Printing Universes is on.