From 679140212d704885f91ec4a23d60628f85bf830a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Sat, 12 May 2018 22:05:23 +0200
Subject: adds a hello world tactic in tuto0

---
 README.md             | 4 +++-
 tuto0/src/g_tuto0.ml4 | 9 ++++++++-
 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
-- 
cgit v1.2.3