aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0/_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/tuto0/_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/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