tuto0/src/g_tuto0.ml4


1
2
3
4
5
6
7

DECLARE PLUGIN "tuto0"

open Pp

VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ]
END