The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 06/26/2012 04:45 AM, Jason Gross wrote: Hi,

Is it possible for [Print Universes] to be wrong?  In my development, after a certain definition (which goes through fine and doesn't give me universe inconsistency errors), if I [Print Universes], I see, among other things,

Category.3 = Category.2

Category.2 < Coq.Init.Logic.17

...

           <= Category.3

 

Hi,
I see nothing wrong with this.
x < y
  <= z
should be understood as x < y /\ x <= z
rather than x < y /\ y <= z

The Print Universes command is very unlikely wrong because it is just a dump of the universe graph. It displays the adjacency matrix rather than chains.

Bruno.