aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/_CoqProject
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-01-07 13:24:14 +0100
committerGaëtan Gilbert2019-01-08 16:41:01 +0100
commitfde557d9e92d2ddd3c79d8a620f2cb33ce64a49f (patch)
tree1b8a0e216119c908d50277432221ab06805a2ac9 /doc/plugin_tutorial/tuto1/_CoqProject
parent8c040974facb733682d24c488dc89941671f4ab7 (diff)
parent168a13dab1c9987f592994150997e692d4d7e40b (diff)
Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e40b'
git-subtree-dir: doc/plugin_tutorial git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7 git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b
Diffstat (limited to 'doc/plugin_tutorial/tuto1/_CoqProject')
-rw-r--r--doc/plugin_tutorial/tuto1/_CoqProject13
1 files changed, 13 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject
new file mode 100644
index 0000000000..585d1360be
--- /dev/null
+++ b/doc/plugin_tutorial/tuto1/_CoqProject
@@ -0,0 +1,13 @@
+-R theories Tuto1
+-I src
+
+theories/Loader.v
+
+src/simple_check.mli
+src/simple_check.ml
+src/simple_declare.mli
+src/simple_declare.ml
+src/simple_print.ml
+src/simple_print.mli
+src/g_tuto1.mlg
+src/tuto1_plugin.mlpack