The Coq mailing list

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

Hi Sam,

> If you change ``integer'' to ``constr'' in the definition of my_induction, 
> then you no longer get the error.

Yes, the error disappears, and it seems to work, but appearances are deceiving
I think. Here's a slightly extended example:

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

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

Inductive weird : nat -> Prop :=
  | weird_0 : weird 0
  | weird_1 : weird 1
  | weird_2 : weird 2
  | weird_3 : weird 3.

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

Now, 

  induction 2.

will do induction on 'weird n' (and give 4 subgoals). my_induction 2 however
will do induction on 'even n' (it seems its completely ignoring the argument);
Thomas's "solution" does the same (induction on 'even n').

Edsko