aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/_CoqProject
diff options
context:
space:
mode:
authorYves Bertot2019-01-11 09:16:48 +0100
committerGitHub2019-01-11 09:16:48 +0100
commitac8c25a9fac51745f0b53162fba48ef5b86d227d (patch)
treef7adb36b9519b9f957cca241767288518da70328 /doc/plugin_tutorial/tuto2/_CoqProject
parent44d767bc5f0f32d5bd7761e81ef225d96ab117b7 (diff)
parentcb2ee2d949899a897022894b750afd1f3d2eb478 (diff)
Merge pull request #8778 from SkySkimmer/merge-plugin-tuto
Move plugin tutorial to Coq repo
Diffstat (limited to 'doc/plugin_tutorial/tuto2/_CoqProject')
-rw-r--r--doc/plugin_tutorial/tuto2/_CoqProject6
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto2/_CoqProject b/doc/plugin_tutorial/tuto2/_CoqProject
new file mode 100644
index 0000000000..cf9cb5cc26
--- /dev/null
+++ b/doc/plugin_tutorial/tuto2/_CoqProject
@@ -0,0 +1,6 @@
+-R theories/ Tuto
+-I src
+
+theories/Test.v
+src/demo.mlg
+src/demo_plugin.mlpack