The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

I am not sure there is any way to flag the culprits, because often,
you agree to let existential variables exist up to some point where
you want them to have disappeared, and then, it is too late.

However, there are two "solutions" I know of:
- use a "feature" of abstract [1]. Using the script [abstract my_tac]
will fail, if [my_tac] leaves non-instantiated existential variables.
- use the vernacular Existential [2]. This allow you to solve by hand
the existential variables, even after the last sub-goal was closed,
and before the Qed.

The very same kind of situation (with a shorter script, though)
occured during an exercise at OPLSS, beginning of the summer, and
using one of the two above solutions worked. However, there may also
be some features of eauto that would allow you to do what you want.

Cheers,
Thomas

[1] But, one may wish for this behavior to change, see
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2386
[2] 
http://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#@command188


On Tue, Jul 26, 2011 at 11:08 AM, Kenneth Roe 
<kendroe AT hotmail.com>
 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?
>
>                               - Ken
>