tuto0/src/g_tuto0.ml4


1
2
3
4
5

open Pp

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