The Coq mailing list

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

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?

The problem, I think, is avoiding goal duplication. Whenever I tried it had some unpleasant effect and I decided to avoid trying something hackish.
 

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 ].

You are right that this is a problem. I'm not sure how to solve that. I'll look into it soon.