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

---
 tuto0/src/g_tuto0.ml4 | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tuto0/src')

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