The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The general solution I use is a tactic I call set_evars:

Ltac set_evars :=

  repeat match goal with

         | [ |- context[?ev] ] => is_evar ev; let e := fresh "e" in set (e := ev)

         end.

The rewrite tactic will not unfold these context definitions to find the evars underneath them.

On Mon, Dec 3, 2018, 05:49 Emilio Jesús Gallego Arias <e AT x80.org> wrote:

Robbert Krebbers <mailinglists AT robbertkrebbers.nl> writes:

> For this concrete example, it appears that the ssreflect rewrite
> tactic is doing what you want (i.e. it does _not_ instantiate the evar
> with []). I have no idea if this is coincidental, or an explicit
> feature of the ssreflect rewrite tactic.
>
> Maybe some of the ssr developers around here could tell more.

See p. 44, Sec 7.2 of https://hal.inria.fr/inria-00258384v17:

,----
| Existential metavariables and rewriting
|
| The rewrite tactic will not instantiate existing existential
| metavariables when matching a redex pattern
`----

Cheers,
E.