The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

One solution is to split the theorem into several lemmas.

Vladimir.


On Jun 29, 2012, at 3:02 AM, Jason Gross wrote:

> Hi,
> I'm trying to diagnose an "Illegal application (Type Error)" that I get on 
> [Qed].  I'm pretty sure it comes from an implicit coercion or from a 
> [rewrite] or from [reflexivity], but I'm not sure.  Is there a way to ask 
> Coq to see if the proof built up so far type-checks?  I can use [admit. 
> Qed.], but this only works if there are no remaining existential variables.
> Thanks.
> 
> -Jason