The Coq mailing list

["Vincent Siles" <vsiles AT lix.polytechnique.fr>]

> Hello,
>
> I wanted to define a tactical working like
>   destruct H as J1 J2 ...
> The list of names of J's is with variant length.  I defined:
>

Hi,
I think you are a bit wrong here:
destruct _ as _ does not take a list of name, but a "intro pattern"[1]
which is a single object that explains how to name the differents parts
of the destructed hypothesis.

However, I don't know how to handle them in Ltac, sorry.

Cheers,
Vincent




[1] 
http://coq.inria.fr/refman/Reference-Manual011.html#@tactic82