The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 04/22/2017 02:55 PM, Kenneth Roe wrote:
> Theorem refl: exists x, x=3+4.
> Proof.
>      apply ex_intro.
>      (* vm_compute. *)
>      compute.
>      reflexivity.
> Qed.

One way to go is to match the goal

Theorem refl: exists x, x=3+4.
Proof.
match goal with |- exists _, _ = ?X =>
  let y := eval vm_compute in X in
  exists y; reflexivity
end.
Qed.