The Coq mailing list

["Jean.Duprat" <duprat AT ens-lyon.fr>]

Dear Eugene,

It seems to me that your problem has its origin in the ambiguity about 
the interpretation of the word "match".

This word is used both by Gallina and Ltac. So, in your tactic

match goal with [ |- match ?n with _ end ] => destruct n end.

the two "match" are interpreted in the same langage Ltac, when you want 
that the first be in Ltac and
the second in Gallina. Try for example the tactic

match goal with [ |- _ = ?n ] => destruct n end.

you obtain what you expect.

Unfortunately, I don't know any way to rise this ambiguity, but I don't 
know all the possibility of Coq.

Yours

   Jean Duprat

Eugene Kirpichov wrote:

> Hello, coq-club.
>
> Suppose I'm proving the following theorem.
> Theorem t : forall n, match n with | O => O | S x => S x end = n.
>  intros n.
>
>  (* Here I could just do "destruct n", but I'd like to do that automatically 
> *)
>
>  match goal with [ |- match ?n with _ end ] => destruct n end.
>
> This doesn't work. Replacing _ with _ => _ doesn't work, either, and
> neither does work anything that I managed to invent.
>
> Is there a way to achieve what I'm trying to do? namely, say,
> "destruct" all variables that are being the head of a match?
>
>