The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Lauri Alanko wrote:
> I'm wondering about the prospects of universe polymorphism in Coq. The
> idea has been around for ages, and every now and then someone stumbles
> into a universe inconsistency while trying to do neat self-referential
> tricks, so obviously there would be use for the feature.

You can often get around this by turning on -impredicative-set and using 
Set in place of Type.  You get the restrictions on elimination of large 
inductive types, but often you can work around them.