The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

You can also do
Set Printing All. Show Proof.
and the copy the output to paste it into a Check command. This should tell 
you 
the point where the problem comes from.
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France


On Friday 29 June 2012 09:03:11 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