aboutsummaryrefslogtreecommitdiff
path: root/tuto1/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to 'tuto1/_CoqProject')
-rw-r--r--tuto1/_CoqProject4
1 files changed, 2 insertions, 2 deletions
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index ce14ee2b87..585d1360be 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -9,5 +9,5 @@ src/simple_declare.mli
src/simple_declare.ml
src/simple_print.ml
src/simple_print.mli
-src/g_tuto1.ml4
-src/tuto1_plugin.mlpack \ No newline at end of file
+src/g_tuto1.mlg
+src/tuto1_plugin.mlpack