The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Is it possible to define a tactic that at some point calls 'induction n' for
some natural number 'n'? I've tried

Tactic Notation "my_induction" integer(n) :=
  induction n.

Inductive even : nat -> Prop :=
  | even_zero : even 0
  | even_succ : forall n, even n -> even (S (S n)).

Lemma foo : forall (n:nat), even n -> True.
Proof.
  my_induction 1.

but that gives (coq 8.2):

In nested Ltac calls to "my_induction'" and "n"), last term evaluation
failed.
Error: Variable n should be bound to a term.

Is there a way to write my_induction?

Edsko

BTW There seems to be an extraneous bracket in the error message :)