The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.31

           <= Coq.Init.Specif.3

           <= Coq.Init.Logic.4

           <= Coq.Init.Specif.5

           <= Category.34

           <= Coq.Init.Datatypes.39

           <= Coq.Init.Datatypes.40

           <= Coq.Init.Logic.166

           <= Category.1826

           <= Coq.Logic.FunctionalExtensionality.16

           <= Coq.Init.Logic.74

           <= Coq.Init.Logic.75

           <= Coq.Init.Logic.76

           <= NaturalTransformation.15

           <= Coq.Logic.FunctionalExtensionality.15

           <= Category.3

           <= Coq.Logic.JMeq.65

           <= Functor.23

           <= Coq.Logic.JMeq.1

           <= Category.1838

The Category.2 < ... <= Category.3 pre-dates the relevant definition; [Print Universes] before the definition includes

Category.2 < Coq.Init.Logic.17

           < Category.31

           <= NaturalTransformation.15

           <= Coq.Logic.FunctionalExtensionality.15

           <= Category.3

           <= Coq.Logic.JMeq.65

           <= Functor.23

           <= Coq.Logic.JMeq.1

           <= Category.1838

Is this a bug in [Print Universes] or in Coq's universe consistency checker, or am I mis-reading the output of [Print Universes]?

-Jason