The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

Dear Coq club,

In my current development of separation logic I rely heavily on type classes, 
in a very similar style to work by Spitters et al. I run into similar 
problems that they did that universe inconsistencies crop up quite regularly. 
I find these exceptionally difficult to debug. Coq will readily tell me which 
the offending types are, but to infer the circle (or find out which 
definitions use these types) the only way that I have found is to print the 
universes and manually check the levels and for large developments this 
doesn't really work.

I understand that a lot of work has recently gone into fixing this for the 
HoTT crowd, and I was wondering if any of this is making it into the standard 
Coq distribution. For the moment, I would be absolutely fine with an option 
to just disable the universe checking. To my mind this is analogous to an 
admit -- it's not something that should be in the end product, but it's 
perfectly fine to use for development purposes. There was a patch to this 
effect for Coq 8.3pl3. Is there something similar now?

Best regards

/Jesper