The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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.

On 11/06/2014 01:38 PM, Robbert Krebbers wrote:
> Tactics like destruct accepts terms with holes for their arguments. For
> example:
>
>    Goal forall x, 1 + 2 = x -> False.
>    intros.
>    destruct (1 + _) eqn:?.
>    Abort.
>
> Here, I am allowed to put an "_" instead of the 2, and Coq will infer
> it. Especially if one has to deal with very large terms, this is
> extremely useful.
>
> Now I want to use destruct as part of an Ltac tactic, and be able to use
> underscores in arguments to the Ltac tactic as well. However, that does
> not seem to work:
>
>    Ltac my_destruct z := destruct z eqn:?.
>
>    Goal forall x, 1 + 2 = x -> False.
>    intros.
>    Fail my_destruct (1 + _).
>    (* Cannot infer this placeholder. *)
>    Abort.
>
> I tried to play around with tactic notation, but without luck:
>
>    Tactic Notation "my_destruct_alt" open_constr(z) := destruct z eqn:?.
>
>    Goal forall x, 1 + 2 = x -> False.
>    intros.
>    my_destruct_alt (1 + _).
>    (* Now I have a meta in Heqn *)
>    Abort.
>
> Any suggestions?