The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael Shulman wrote:
> I am trying to do one of the exercises in the book CPDT (namely, 7.5
> about plists) and I am getting the error "No more subgoals but
> non-instantiated existential variables".  The only documentation I can
> find about this error says "This means that eauto or eapply didn't
> instantiate an existential variable which eventually got erased by some
> computation."  But I never used eauto or eapply in my proof!  Can they
> be hiding somewhere?  How can I track down the problem?  I can post my
> particular code if that would help, but I would mostly like to know what
> could be going on in theory.
>    

I'm not sure what's going on, either, but the command [Show 
Existentials.] will print which existentials are left and what contexts 
they were created in.  That should provide a clue.