Universe information

[Alizter]

It is currently quite awkward to extract information about universes in Coq. During a proof, one typically has to resort to Show Universes to understand which universes are present. It might be useful to have a (minimized by default) window in the goals window to see the universe information. Essentially something that outputs Show Universes at each stage.

[ejgallego]

That seems like a good idea, why not?

Can you point out some proof that you would consider representative of your use case?

[Alizter]

In HoTT we have Algebra/Rings/Matrix.v and typically after a rewrite there are many superfluous universe variables that get generated and then flattened at Defined.

[ejgallego]

That's interesting, maybe work reporting upstream?

Allow me some questions because I don't know this stuff very well, what's the typical workflow for this case?

1. you do the rewrite
2. you look at the universes
3. then?