Declare ML Module "evil_plugin".

magic.

Lemma x : True. Proof. trivial. Qed.