test-suite/bugs/closed/bug_4453.v


1
2
3
4
5
6
7
8
9
10

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