diff options
| author | Yves Bertot | 2018-05-04 16:04:54 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 16:04:54 +0200 |
| commit | cb20f241cc7ec686a5ae19c1e7b9eef6b26d230a (patch) | |
| tree | ec56b21410c26c23601b48890515a6eb6534014c | |
| parent | eba06e2192d88af463fb6dec85e2f039a0a13694 (diff) | |
adds more packaging boilerplate in tuto0
| -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 |