The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

I examine the differences between the and_rect and prod_rect definition (with Print and_rect and Print prod_rect).
In the and_rect definition, you have P:Type while in the prod_rect definition, you have P: prod A B -> Type.
Why is the reason of this difference ?

-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy