The Coq mailing list

[Xavier Leroy <xavier.leroy AT inria.fr>]

On 23/07/2014 10:44, Arnaud Spiwack wrote:
> Coq has a lot of backstory and stuff. So the treatment of existential
> variables is not superbly uniform. In trunk, the [refine] tactic
> introduces existential variable as goals. It is the preferred way to
> manipulate existential variable explicitly.

I don't enjoy counting evar occurrences from the right any more than
you, but there is one situation where I often have to use instantiate:
after a "erewrite", to fix up some of the evars this tactic introduced.
AFAIK, there is no "erewrite ... with (var := value)" like there is
for "eapply".

> But hopefully, we can get rid of [instantiate] eventually: it's not
> a very elegant solution.

Make sure you have decent alternatives for all current uses of
"instantiate" before your sense of elegance takes over.  Thanks in
advance.

- Xavier Leroy