The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.

Here's a groaty "solution": use [instantiate] to set any well-typed 
values of those existentials, then use the trick you mentioned.