The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Vladimir,

[as] should do the trick. If you try:

==========
Goal forall (n: nat), True.
intro n ; induction n as [| m Hp].
 apply I.
==========

you will see that the variable is named [m] and the induction
hypothesis is [Hp]

Cheers,

--
guillaume



On 28 June 2011 21:42, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> Hello,
>
> is there a way to prescribe explicitly the names of all the variables 
> introduced by the tactic command [ induction n ] in the case when [ n : nat 
> ] ?
>
> Thanks!
> Vladimir.
>
>
>
>