The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

On Thu, Apr 19, 2012 at 07:18:58AM +0200, Andrej Bauer wrote:
> 
> First, casting to "Type" is not a type annotation because Type is not
> a type... 

First could I say that I've found reading this thread very useful in 
understanding the Type heirarchy. (Yes, I know it's in the docs!)
It does strike me, however, that someone might want to define something to be 
at a particular place, e.g. Type(3) or above.

Regards,

Bernard.