The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Kenneth Roe wrote:
> I have a proof that is a few hundred lines, involves many (nested) Coq 
> calls, and takes about 15 minutes to complete.  At the end, I have the 
> error "No more subgoals but non-instantiated existential 
> variables:...".  What is the fastest way to find the exact lines of 
> source code that are generating these goals?

One approach I've used is binary search with the placement of [Show 
Existentials.] within the proof script. ;)