diff options
| -rw-r--r-- | README.md | 4 | ||||
| -rw-r--r-- | tuto0/src/g_tuto0.ml4 | 9 |
2 files changed, 11 insertions, 2 deletions
@@ -4,7 +4,9 @@ How to write plugins in Coq # tuto0 : basics of project organization package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - - Example of function call to print a simple message. + - Example of function call to print a simple message + - Example of syntax to add a simple tactic + (that does nothing and prints a message) - To use it: ```bash diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4 index e3656fc986..df6e187d52 100644 --- a/tuto0/src/g_tuto0.ml4 +++ b/tuto0/src/g_tuto0.ml4 @@ -1,7 +1,14 @@ DECLARE PLUGIN "tuto0" open Pp +open Ltac_plugin VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY | [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ] -END
\ No newline at end of file +END + +TACTIC EXTEND hello_world_tactic +| [ "hello_world" ] -> + [ let _ = Feedback.msg_notice (str Tuto0_main.message) in + Tacticals.New.tclIDTAC ] +END |