test.v « theories « template « coq-makefile « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/coq-makefile/template/theories/test.v

blob: 744b5aad7838b09bc5574fac097d1064c8dedb85 (plain)

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