The Coq mailing list

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

I agree. I meant I was not sure how to implement this very feature. You can indeed make a bug report, it will help if the solution is not found quickly.

On 25 July 2014 15:41, Jason Gross <jasongross9 AT gmail.com> wrote:

On Fri, Jul 25, 2014 at 12:55 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

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.

It might be nice, in general, if binders respected fresh.  For example,

Goal True.

Proof.

  let H := fresh "E" in

  pose (fun H : Set => H).

should give me [fun E : Set => E], not [fun H : Set => H].  I think this would be enough to solve the problem.  Should I make a bug report?