aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto3/_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/tuto3/_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/tuto3/_CoqProject')
-rw-r--r--doc/plugin_tutorial/tuto3/_CoqProject12
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/tuto3/_CoqProject b/doc/plugin_tutorial/tuto3/_CoqProject
new file mode 100644
index 0000000000..e2a60a430f
--- /dev/null
+++ b/doc/plugin_tutorial/tuto3/_CoqProject
@@ -0,0 +1,12 @@
+-R theories Tuto3
+-I src
+
+theories/Data.v
+theories/Loader.v
+
+src/tuto_tactic.ml
+src/tuto_tactic.mli
+src/construction_game.ml
+src/construction_game.mli
+src/g_tuto3.mlg
+src/tuto3_plugin.mlpack