diff options
Diffstat (limited to 'tuto0/src')
| -rw-r--r-- | tuto0/src/g_tuto0.ml4 | 4 | ||||
| -rw-r--r-- | tuto0/src/tuto0_main.ml | 1 | ||||
| -rw-r--r-- | tuto0/src/tuto0_main.mli | 1 | ||||
| -rw-r--r-- | tuto0/src/tuto0_plugin.mlpack | 1 |
4 files changed, 6 insertions, 1 deletions
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4 index 5e0fa36e51..e3656fc986 100644 --- a/tuto0/src/g_tuto0.ml4 +++ b/tuto0/src/g_tuto0.ml4 @@ -1,5 +1,7 @@ +DECLARE PLUGIN "tuto0" + open Pp VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY -| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk "Hello World!") ] +| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ] END
\ No newline at end of file diff --git a/tuto0/src/tuto0_main.ml b/tuto0/src/tuto0_main.ml new file mode 100644 index 0000000000..93a807a800 --- /dev/null +++ b/tuto0/src/tuto0_main.ml @@ -0,0 +1 @@ +let message = "Hello world!" diff --git a/tuto0/src/tuto0_main.mli b/tuto0/src/tuto0_main.mli new file mode 100644 index 0000000000..00d981ad75 --- /dev/null +++ b/tuto0/src/tuto0_main.mli @@ -0,0 +1 @@ +val message : string
\ No newline at end of file diff --git a/tuto0/src/tuto0_plugin.mlpack b/tuto0/src/tuto0_plugin.mlpack index 9360e6036e..02bc329591 100644 --- a/tuto0/src/tuto0_plugin.mlpack +++ b/tuto0/src/tuto0_plugin.mlpack @@ -1 +1,2 @@ +Tuto0_main G_tuto0
\ No newline at end of file |