The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/09/2014 06:54 PM, Robbert Krebbers wrote:
> Arnoud, Jonathon: thanks for the replies.
>
> Inspired by Jason's message on splitting evars, I ended up with
>
> Tactic Notation "my_destruct" open_constr(z) :=
>   match goal with
>   | _ : context [?z'] |- _ => unify z z'; destruct z
>   end.
>
> Goal forall x, 1 + 2 = x -> True.
>   intros.
>   my_destruct (_ + _).
>   Restart.
>   intros.
>   my_destruct (1 + _).
>   auto.
>   auto.
> Qed.
>
> This seems to work, even on Coq 8.4.

So that undocumented open_constr has been around at least since 8.4?  Sigh.

-- Jonathan