The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT loria.fr>]

On Tue, 17 Jan 2006, Adam Chlipala wrote:

> Is this really a problem?  In my long journey towards understanding the 
> metatheory of Coq, I've come to explain to myself the distinction among 
> Set/Prop/Type as only being necessary to support extraction.  Do you really 
> need more than the different levels of Type if you're only interested in 
> checking proofs in the simplest possible calculus?

the Type hierarchy is predicative while Prop is impredicative. this means that 
(forall P : Prop, P => P) is of type Prop, while (forall P : Type_i, P => P) 
is of type Type_i+1. i explicitly added the indexes which are not printed by 
coq.