The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> In 8.2 Prop=Set is provable by firstorder. This doesn't work in 8.3.

Well spotted. This is a bug introduced in 8.2, that was fixed for 8.3
but unfortunately not backported to 8.2. We'll do a patch level
release for 8.2 soon to make the fix available.

> Yet all of this are provable in 8.3:
> exists a : Set,a=True:Prop. 
> exists a : Prop,a=True:Prop. 
> exists! a : Type, a=True:Prop.
> 
> Is [Prop=Set] in 8.3 too ?
> 
> Definition FA := True:Prop.
> 
> Lemma set0: exists a : Set,a=FA.
> eexists. firstorder.
> Qed.
> 
> Lemma prop0: exists a : Prop,a=FA.
> eexists. firstorder.
> Qed.
> 
> Lemma typeuniq: exists! a : Type, a=FA.
> eexists. firstorder.
> Qed.

These ones are harmless.

Hugo Herbelin