The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Hi Keiko, 
On Wed, 09 Jul 2008 17:33:54 +0900 (JST)
Keiko Nakata 
<keiko AT kurims.kyoto-u.ac.jp>
 wrote:

> 
> > 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.  
In practice, you can suspect new tactics (which are less tested than
old tactics) and tactics which have changed a lot recently. Some months
ago, I had a problem with rewrite (before Matthieu's changes), I
personally use some unsafe features as the fix tactic when creating
Function principles (but I can not break your proof since this part is
closed by its own qed). I suspect that some uses of eapply may lead to
wrong typed term. 
Can you send us the exact error message ? 


Best regards, 
Julien