The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

Sorry, this was nonsense:

Samuel E. Moelius III wrote:
> It appears that, at the prompt, ``induction 2'' invokes the following 
> version of ``induction'' from page 176 of the 8.2 reference manual.

I realize now that you intended the version of ``induction'' described at 
the top of page 174.

I think that the following may be a work-around.

(*=======================================================================*)

Tactic Notation "my_induction" integer(n) :=
  intros until n;
  induction 0.

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 foo0 : forall (n:nat), even n -> weird n -> True.
Proof.
  my_induction 2.
  (**)tauto.
  (**)tauto.
  (**)tauto.
  (**)tauto.
Qed.

Lemma foo1 : forall (n:nat), even n -> weird n -> True.
Proof.
  my_induction 1.
  (**)tauto.
  (**)tauto.
Qed.

(*=======================================================================*)

Still, it is odd that ``induction n'' doesn't just work.

Best,

Sam