The Coq mailing list

[Randy Pollack <rap AT dcs.ed.ac.uk>]

Oops.  In my last message I suggested that Coq V7 did better job at
universe polymorphism than Coq V6.3.1.  Another experiment shows that
Coq V7 accepts too much: 

 Reset Initial.
 Parameter K: (T:Type)T->T.
 Check (K ((T:Type)T->T) K).

This is accepted by Coq V7.0beta, but should be rejected.  There is no
question of polymorphism here, as K is a parameter, not defined.

Randy