The Coq mailing list

[Anthony Bordg <bordg.anthony AT gmail.com>]

Hi,

 the tactic "intros until ident"  can't be of any help here ? (see https://coq.inria.fr/distrib/current/refman/Reference-Manual010.html#hevea_tactic29).

Best

Le samedi 7 février 2015 16:00:30 UTC+1, v v 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.

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.