The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, I don't think there is any built in way to do that (chaining Show Proof with Check doesn't work unfortunately, because Coq doesn't parse existential variables, they are only printed). But it sounds easy enough to to add. Should we?

On 29 June 2012 12:08, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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