The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Yes, you can use intro pattern to do this.
For example, if you are destructing a list, you can write

destruct l as [ | hd tl ].

which means: destruct l. For the first constructor, do nothgin, for
the second, do 2 introductions
with the names hd and tl.

Cheers,
Vincent


2011/4/17 Vladimir Voevodsky 
<vladimir AT ias.edu>:
> Is it possible to tell the "destruct" tactic  which names to choose for the 
> new variables which it introduces?
>
> Thanks!
> Vladimir.
>
>
>
>
>