The Coq mailing list

[Vincent BENAYOUN <benayoun.vincent AT gmail.com>]

Hi all,

I need to use the tactic "induction term eqn:naming_intro_pattern" in some of my proofs but I get an error message.

Here is a simplified version of my problem.

If I remove "eqn:toto" from the following proof it works perfectly.

But why does it fail with "eqn:toto" ???

Inductive bbb : nat -> Prop :=

| BBB : bbb 0.

Lemma bbb_theorem :

  forall (n:nat), bbb n -> n = 0.

Proof.

  intros n HHH.

  induction HHH eqn:toto.

  reflexivity.

Qed.

Thanks,

Vincent