The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

I have a simple query about using Ltac. I'm trying to write a tactic which 
makes use of "destruct" and want to be able to name the new variables 
introduced into the context e.g. "destruct x as [|head tail]" instead 
of "destruct x". I tried this Ltac tactic:

Ltac mydestruct o x := destruct o as x.

But it doesn't work:

Definition test : list nat -> list nat.
intros x.
(* mydestruct x [|head tail].  (* doesn't work *) *)
destruct x as [|head tail]. (* works *)

How do I say in Ltac that "x" should be an introduction pattern? Also, are 
there any good sources for answers to questions like this about Ltac?

Regards,

Sean