The Coq mailing list

[vsiles AT lix.polytechnique.fr]

Hi,
by using the tactic "fix" without being cautious, you can complete a proof
but the Qed failed, mostly because your recursive call was not on a sub
term.

That's the only case I know where Qed can failed.

I hope it'll help a little.

Vincent

> Hello.
>
> Is it possible that "Qed" ends up with a type error,
> or other serious errors except for the out of memory?
> I never omit to instantiate existential variables,
> no metavariables are left (e.g. no eauto or eapply),
> or I do not use co-induction.
>
> Currently I do not want to struggle with the out of memory problem
> which I incur by Qed, but I want to be sure my proof term is correct.
>
> With best regards,
> Keiko
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>