The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail