diff options
| -rw-r--r-- | tuto0/_CoqProject | 3 | ||||
| -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 | ||||
| -rw-r--r-- | tuto0/theories/Loader.v | 1 |
6 files changed, 10 insertions, 1 deletions
diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject index 2871fcd549..ca0c0588a4 100644 --- a/tuto0/_CoqProject +++ b/tuto0/_CoqProject @@ -1,5 +1,8 @@ -R theories/ Tuto0 -I src +theories/Loader.v +src/tuto0_main.ml +src/tuto0_main.mli src/g_tuto0.ml4 src/tuto0_plugin.mlpack
\ No newline at end of file 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 diff --git a/tuto0/theories/Loader.v b/tuto0/theories/Loader.v new file mode 100644 index 0000000000..583b77dc3b --- /dev/null +++ b/tuto0/theories/Loader.v @@ -0,0 +1 @@ +Declare ML Module "tuto0_plugin".
\ No newline at end of file |