The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Instantiate deprecated?  I thought that was the way to handle evars manually.  How else?

Kinda sorta… ish.

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.

For instance, instead of [evar (P:Prop)], you can use [refine (let P:Prop := _ in _)] and get two goals: one for your goal with a new binding [P := ?x : Prop], and one (the first one actually) of type [Prop], whose solution will instantiate [?x] (and vice-versa, if [?x] is partially instantiated, the goal will be considered solved).

Now, it may not fit your needs. Since the new refine is new, and the possibilities are largely unexplored and suffer from limited support, you may still need [instantiate]. But hopefully, we can get rid of [instantiate] eventually: it's not a very elegant solution.