aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile/coqdoc1/theories/test.v
blob: 7753b56aae252ff95d5c3b9651e6f936c60d074c (plain)
1
2
3
4
5
6
7
Declare ML Module "test_plugin".
Test.
Goal True.
Proof.
test.
exact I.
Qed.