diff options
Diffstat (limited to 'test-suite/coq-makefile/template/src/test.mlg')
| -rw-r--r-- | test-suite/coq-makefile/template/src/test.mlg | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/template/src/test.mlg b/test-suite/coq-makefile/template/src/test.mlg new file mode 100644 index 0000000000..7a166f3b98 --- /dev/null +++ b/test-suite/coq-makefile/template/src/test.mlg @@ -0,0 +1,18 @@ +{ +open Ltac_plugin +} +DECLARE PLUGIN "test_plugin" +{ +let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; +} + +VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF + | [ "TestCommand" ] -> { () } +END + +TACTIC EXTEND test +| [ "test_tactic" ] -> { Test_aux.tac } +END + + + |