aboutsummaryrefslogtreecommitdiff
path: root/tuto0/_CoqProject
diff options
context:
space:
mode:
authorYves Bertot2018-05-01 21:30:53 +0200
committerYves Bertot2018-05-01 21:30:53 +0200
commitb5c0be9687aad69913e24354a041f188ee25efaf (patch)
tree210789d582f5d0220ab95713c2769fd4b4c550c3 /tuto0/_CoqProject
a first project on how to organize files and define a simple query
Diffstat (limited to 'tuto0/_CoqProject')
-rw-r--r--tuto0/_CoqProject5
1 files changed, 5 insertions, 0 deletions
diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
new file mode 100644
index 0000000000..2871fcd549
--- /dev/null
+++ b/tuto0/_CoqProject
@@ -0,0 +1,5 @@
+-R theories/ Tuto0
+-I src
+
+src/g_tuto0.ml4
+src/tuto0_plugin.mlpack \ No newline at end of file