How to debug universes?

1. There is a command Print Universes in Coq toplevel

   Print Universes.
     prints the graph of universes in the form of constraints

   Print Universes "file".
     produces the "file" containing universe constraints in the form
       univ1 # univ2 ;
     where # can be either > >= or =

   If "file" ends with .gv or .dot, the resulting file will be in
   dot format.


   *) for dot see http://www.research.att.com/sw/tools/graphviz/


2. There is a printing option

   {Set,Unset} Printing Universes.

   which, when set, makes all pretty-printed Type's annotated with the
   name of the universe.