The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

thank you.

sorry.

On Wed, May 25, 2011 at 10:51:29PM +0800, Jean-Francois Monin wrote:
> This is a well-known feature. "Proof completed" just means that you
> don't have subgals left, but says nothing about guardedness.
> Usual tactics don't raise this issue, but fix does.
> BTW this tactics is not documented, for some reason...
> 
> This is just like writing
> 
> Fixpoint l3 (H: CC) : False := l3 H.
> 
> So if you happen to try it, you must know what you are doing and not 
> complain.
> 
> JF
> 
> On Wed, May 25, 2011 at 05:34:16PM +0300, Georgi Guninski wrote:
> > coqtop gives misleading message:
> > u
> > 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.