The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

>>> 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 not agree completely with Vincent. In theory, all tactics may lead
> to type error at Qeq since the only critical phase
> w.r.t. typechecking is Qed.

Here is an example that I ran into a couple of years ago:
proving "4294967296 = 0" using the omega tactic.  At that time, omega
was implemented using Caml's native integer arithmetic (modulo 2^31 on
a 32-bit machine).  To omega, the goal looked like "0 = 0", the proof
term produced was (refl_equal 0), and of course Qed rejected it as not
of the correct type...

I hasten to add that since 8.1 (I think), omega uses exact integers
and I never ran into this problem again.

Coming back to Keiko's issue, looking long and hard at the type error
message reported by Qed, then replacing parts of the script by
"admitted" could possibly give a clue on which tactic produces the
faulty proof term.

- Xavier Leroy