adds a hello world tactic in tuto0

2 files changed, 11 insertions, 2 deletions

diff --git a/README.md b/README.md
index 417a511f82..64d4241360 100644
--- a/README.md
+++ b/README.md
@@ -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