The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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