diff options
| author | Yves Bertot | 2018-05-12 22:05:23 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-12 22:05:23 +0200 |
| commit | 679140212d704885f91ec4a23d60628f85bf830a (patch) | |
| tree | 8384a59be5a3a381ea197b9911d67f937f34d4d9 /tuto0/src | |
| parent | d558653e3a0ecc0b182f5e84a8db474d7a5aa1f8 (diff) | |
adds a hello world tactic in tuto0
Diffstat (limited to 'tuto0/src')
| -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 |