aboutsummaryrefslogtreecommitdiff
path: root/tuto3/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to 'tuto3/_CoqProject')
-rw-r--r--tuto3/_CoqProject4
1 files changed, 2 insertions, 2 deletions
diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 6a3c1978a7..e2a60a430f 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -8,5 +8,5 @@ src/tuto_tactic.ml
src/tuto_tactic.mli
src/construction_game.ml
src/construction_game.mli
-src/g_tuto3.ml4
-src/tuto3_plugin.mlpack \ No newline at end of file
+src/g_tuto3.mlg
+src/tuto3_plugin.mlpack