The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

Jason Gross 
<jasongross9 AT gmail.com>
 writes:

> Hi,
> I noticed that Coq seems to have had universe polymorphism at one point,
> but no longer does (see commit message at the bottom of the message).  Is
> there somewhere that I can find an explanation of why this was removed, or
> can someone respond with an explanation?  (If it was discussed on coq-club
> before, are there archives of coq-club@, and can someone point me to them?)

coq has for a long time had a limited support for universe polymorphism
for inductive types. The commit you reference was an attempt at adding
more support, but it wasn't actually effective (hence the revert).

  Tom