The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

Le 07/02/2015 16:00, Vladimir Voevodsky a écrit :
> Hello,
>
> is there a nice way to ask Coq to do the intros up to (and including) the 
> variable whose name is ident?
>
> E.g. I may have many parameters in a lemma and one of them in the middle is n 
> and I want to do induction in n after having introduced the variables up to n 
> but not the ones after n.
Doesn't "induction n" work?

Frédéric.
> At the moment I say “intros ident_1 …. ident_i n.” but it would produce less 
> fragile code if I could say “intros_up_to n.”
>
> Vladimir.