aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to 'doc/plugin_tutorial/tuto0/_CoqProject')
-rw-r--r--doc/plugin_tutorial/tuto0/_CoqProject10
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto0/_CoqProject b/doc/plugin_tutorial/tuto0/_CoqProject
new file mode 100644
index 0000000000..76368e3ac7
--- /dev/null
+++ b/doc/plugin_tutorial/tuto0/_CoqProject
@@ -0,0 +1,10 @@
+-R theories/ Tuto0
+-I src
+
+theories/Loader.v
+theories/Demo.v
+
+src/tuto0_main.ml
+src/tuto0_main.mli
+src/g_tuto0.mlg
+src/tuto0_plugin.mlpack