The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi, 

Just a remark. As I mentioned before in my previous email, I keep
getting universe inconsistencies. Now, I was aware of the 

  Set Printing Universes.

command, but it never seemed to do anything for me. Both the Cocorico
wiki and the Coq manual say to follow this command up with

  Print Universes.

which indeed shows the universe constraints, but it doesn't tell me what
universe variables correspond to which terms. It wasn't obvious to me
that I could see that using the normal Print option, for example

  Print prod.

I was actually on the verge of trying to modify the Coq sources to tell
me what universe variables correspond to which terms when I found out
that Set Printing Universes in combination with Print does exactly that.
A pleasant surprise indeed! :)

Now, perhaps I'm the only one not to make the connection, but perhaps
not -- it might be useful to make this explicit (maybe show an example)
in the manual/on the wiki?

Edsko