test-suite/bugs/closed/4453.v


1
2
3
4
5
6
7
8


Section Foo.
Variable A : Type.
Lemma foo : A -> True. now intros _. Qed.
Goal Type -> True.
rename A into B.
intros A.
Fail apply foo.