aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_13755.v
blob: cc25157b9be8069cbbafede625410649799f0cba (plain)
1
2
3
4
5
Module M1.
Lemma t1 : True.
Fail End M1.
Proof. exact I. Qed.
End M1.