The Coq mailing list

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

Hi,

> coqtop gives misleading message:
> 
> Inductive CC : Prop := C1: (exists B : Prop,CC)->CC | C2 : True->CC.
> Lemma l3: CC->False.
> Proof.
> fix 1. 
> intros.
> exact (l3 H).
> Qed.
> l3 < Proof completed.
> ^ the above is a lie :)

Indeed, the message is worth to be improved (done in the development
version).

Hugo Herbelin