The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Thu, May 26, 2011 at 01:28:57PM +0200, herbelin wrote:
> 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).
>

thanks. trunk coqtop appears fixed.

trunk coqide still gives "Proof completed" though.