Declare ML Module "test_plugin".
TestCommand.
Goal True.
Proof.
test_tactic.
exact I.
Qed.