ignore Qed/Defined which are not preceded by Proof

Code like:
Definition x : nat.
  exact 0.
Defined.
(without a Proof.) no longer breaks the output.