The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 29/06/2012 09:02, Jason Gross wrote:
> 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.

You may try to fiddle with the Show Proof command, but in the general 
case, I cannot figure out how to typecheck an incomplete proof-term...

PMP