diff options
Diffstat (limited to 'test-suite/coq-makefile/uninstall1/src/test.ml4')
| -rw-r--r-- | test-suite/coq-makefile/uninstall1/src/test.ml4 | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/test-suite/coq-makefile/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4 deleted file mode 100644 index 8ddc9b095..000000000 --- a/test-suite/coq-makefile/uninstall1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -DECLARE PLUGIN "test_plugin" -let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; - -VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "Test" ] -> [ () ] -END - -TACTIC EXTEND test -| [ "test" ] -> [ Test_aux.tac ] -END - - - |