The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Note also that you still get the full elimination principle for Type.
This is explained in the section "Empty and singleton elimination" in
the doc.

Guillaume

2013/2/13 Guillaume Brunerie 
<guillaume.brunerie AT gmail.com>:
> No, that’s a feature.
> See here http://coq.inria.fr/doc/Reference-Manual006.html#@default353
> (further down), and in particular the sentence:
>
>> […] More precisely, an empty or small singleton inductive definition is 
>> set in Prop, a small non-singleton inductive family is set in Set, and 
>> otherwise in the Type hierarchy.
>
> Guillaume
>
> On 2013/2/12 Marco Maggesi 
> <maggesi AT math.unifi.it>
>  wrote:
>> When I try to define in Coq 8.4 the empty Type but I get an empty Prop.
>> Is this a bug?
>> M.
>>
>> Welcome to Coq 8.4 (September 2012)
>>
>> Coq < Inductive empty : Type := .
>> empty is defined
>> empty_rect is defined
>> empty_ind is defined
>> empty_rec is defined
>>
>> Coq < Check empty.
>> empty
>>      : Prop