The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> http://article.gmane.org/gmane.science.mathematics.logic.coq.club/5386
>
>
>   My particular use case -- is that I like to use erewrite -- I specify as little as possible, put in lots of _ _'s, and have the rewrite happen. Then, later, I prove the missing terms.
>

If you only care about filling in existentials at the end of the proof, you can use [Grab Existential Variables.]

-Jason