`evar` should return the created evar

[dhalilov]

Is your feature request related to a problem?

The following innocent-looking Ltac script does not work in general:

Ltac mytac := 
  evar (x : nat);
  unify ?x 0.

As stated in the documentation, evar (x : T) generates a fresh name for the evar, which is confusing in Ltac scripts since that means you cannot simply reference the created evar as ?x. This creates usability issues, as in PrincetonUniversity/VST#834.

Proposed solution

I propose that evar (x : T) returns the created evar, so that one could write this instead:

let x_evar := (evar (x : nat)) in
unify x_evar 0

Alternative solutions

Currently, the work-around is to do the following:

Ltac mytac :=
  evar (x : nat);
  let x_evar := (eval unfold x in x) in
  unify x_evar 0

We could provide some tactic evar_of x that would essentially do eval unfold x in x, but this is a subpar solution in my opinion.

Additional context

This issue was discovered while investigating CI failure for VST in #20809; see in particular PrincetonUniversity/VST#834.

[SkySkimmer]

You can do let x := open_constr:(_ :> nat) in unify x 0
The evar tactic is more for interactive use AFAICT

[dhalilov]

You can do let x := open_constr:(_ :> nat) in unify x 0 The evar tactic is more for interactive use AFAICT

It might be nice to mention that in the docs, especially since evar seems (to a non-expert like me) to be the natural way to create a new evar.