The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all, I found something that I consider a bug:

Section X.
Variable n: nat.
Hypothesis H: n = 0.
Lemma foo: True.
(* induction H. *)
  (*Here I see no real technical reason to forbid it*)
 revert H; intros H.
(* induction H. *)
  (*We try a trick to make it work by making it something
    not a section variable, but it fails*)
 revert H; intros K.
 induction K.
  (*We try a trick to make it work by making it something
    not a section variable, and it succeeds*)
 split.
Qed.
End X.

As I don't see any practical reason of this, I post on the mailing list.
I used 8.3 on FreeBSD.
I didn't tried the trunk version.