blob: d6e95ba0f7e48a42d31823c438921c2012f22854 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
DECLARE PLUGIN "tuto0_plugin"
open Pp
open Ltac_plugin
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ]
END
TACTIC EXTEND hello_world_tactic
| [ "hello_world" ] ->
[ let _ = Feedback.msg_notice (str Tuto0_main.message) in
Tacticals.New.tclIDTAC ]
END
|
