diff options
Diffstat (limited to 'tuto0')
| -rw-r--r-- | tuto0/src/g_tuto0.ml4 | 9 |
1 files changed, 8 insertions, 1 deletions
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 |