The Coq mailing list

[Yves Bertot <Yves.Bertot AT inria.fr>]

On 05/11/2016 06:27 PM, Frédéric Blanqui wrote:
> Hello Yves. Does dpdgraph print universe dependencies too?
No, we did not think of it.  The message "support for universe 
polymorphic constants" only expresses that the previous version would 
break in the presence of universe polymorphic constants.

My impression is that a program printing universe dependencies requires 
a completely different exploration of Coq's database.  It must not be 
too hard to program, as long as we find the right entry points.  Thanks 
for the suggestion.

Yves