1 2 3 4 5 6 7
Declare ML Module "test_plugin". TestCommand. Goal True. Proof. test_tactic. exact I. Qed.