aboutsummaryrefslogtreecommitdiff
path: root/tuto2/_CoqProject
diff options
context:
space:
mode:
authorEnrico Tassi2018-05-17 17:36:44 +0200
committerEnrico Tassi2018-05-17 17:38:13 +0200
commit7f31b7f1ee4d4857aaed86ad7fd6bcbb83e2a705 (patch)
tree79b805c1e2210ab957f2f3596ecc6d07a977dd2e /tuto2/_CoqProject
parent679140212d704885f91ec4a23d60628f85bf830a (diff)
[tuto2] Clarify where the name of the ML plugin is used
Diffstat (limited to 'tuto2/_CoqProject')
-rw-r--r--tuto2/_CoqProject2
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
index f38ee8d6a6..bdafdb5f04 100644
--- a/tuto2/_CoqProject
+++ b/tuto2/_CoqProject
@@ -3,4 +3,4 @@
theories/Test.v
src/demo.ml4
-src/tuto_plugin.mlpack
+src/demo_plugin.mlpack