The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

I just got a new 'error' message from Coq and I would appreciate some words on it :-)

So, happily typing the last tactic so prove a goal, expecting to get my favorite message, instead I got

"No more subgoals but non-instantiated existential variables:

Existential 1 =

?8590439 : [Case := "At Least One Step" : string

            s : state

            H : well_formed s

            ...  |- binding] "

And therefore, Coq does not allow me to Qed.

Practically speaking, this happened because I applied a lemma with 'eapply my_lemma; eauto'. By applying it with explicit parameters I no longer got this message and could conclude the proof.

This particular proof was not that big, and therefore finding what to change to make it work wasn't too much of an headache, but it seems that since I do not get any kind of message/warning whatsoever while doing the proof - and thus no way to predict that this can happen when I will try to Qed - it could potentially get me into hard to "debug" proofs (that are essentially already solved anyway!)

So, what am I missing? Or should I just stay away from 'eapply' and the like?

Thank you fellows!

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.