Module M1.
Lemma t1 : True.
Fail End M1.
Proof. exact I. Qed.
End M1.