The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/06/2014 08:56 PM, Jonathan wrote:
> Actually - it is possible (in the trunk) if one is willing to use a 
> bit of a kludge involving refine, an evar, and eval:
>
>   Tactic Notation "my_destruct" uconstr(p) :=
>   let e := fresh in
>   refine (let e := p in _);
>   [shelve
>   |let v := eval hnf in e in
>    match goal with _ : context[?C] |- _ => unify v C; clear e; 
> destruct C eqn:? end].
>
>   Goal forall x, 1 + 2 = x -> False.
>   intros.
>   my_destruct (1 + _).
>
> -- Jonathan

Oh, sorry, that only handles patterns with a single hole.  Simple fix to 
make it work for any number of holes:

Tactic Notation "my_destruct" uconstr(p) :=
  let e := fresh in
  refine (let e := p in _);
  shelve_unifiable;
  let v := eval hnf in e in
  match goal with _ : context[?C] |- _ =>
    unify v C; clear e; destruct C eqn:?
  end.

Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct (_ + _).

-- Jonathan