The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

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 :)

thank you.