The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Kenneth Roe 
<kendroe AT hotmail.com>
 writes:

   [...] 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?

After running myself into this problem I extended prooftree with
the ability to mark the proof command that introduced a certain
existential variable, see http://askra.de/software/prooftree/

Bye,

Hendrik