The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is the problem the syntax, or the code?  You can already write a [solve evar e using tac] by throwing [tac] into [$(...)$], and then unifying [e] with the result.  If it's the syntax, how about [unshelve e], which leaves you with one additional focused goal at the front?

Also, by the way, is it intended that you have to inspect the hypotheses to get your hands on the name of the evar introduced by [refine (let e : T := _ in _)] in the second goal?  That is, to get a fresh named evar as a goal, I do something like

Ltac new_style_evar e T :=

  refine (let e' : T := _ in _);

  [

  | let e' := match goal with e' := _ |- _ => constr:(e') end in

    rename e' into e ].

On Fri, Jul 25, 2014 at 7:36 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Can one transform an existing evar into such a thing?  Or only those introduced by refine?

 I don't have a good method to transform otherwise introduced existential variables into goals at the moment. Either they were introduced by a refine, or you can use the Grab Existential Variables command when no goal is left to turn all the remaining existential variables into goals.