coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] non-instantiated existential variables

From: Michael Shulman <viritrilbia AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] non-instantiated existential variables
Date: Sat, 06 Mar 2010 13:39:49 -0600
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:subject :content-type:content-transfer-encoding; b=nBKUyyVD5ur5KrBWn+G9jWSi1Dybbq7jIOx3P/WQbSfrmy9jY407304Tn8AfYmS9MN 8lf6V+JhH6/OnbUUam3dOPt7fprca5OmqF9GayRKMXjxqoPqMY7GRrDd0tJh8bDud7Ya /UlSjZlwgHugckynHzBoew0N+6L770foaxa50=

Hi,

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.

Thanks,
Mike

[Coq-Club] non-instantiated existential variables, Michael Shulman
- Re: [Coq-Club] non-instantiated existential variables, Adam Chlipala