aboutsummaryrefslogtreecommitdiff
path: root/tuto0/_CoqProject
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-10-31 17:57:47 +0100
committerPierre-Marie Pédrot2018-11-05 18:36:00 +0100
commit0fe2b5d4d63bcbc63d48a386949094c23e4c274e (patch)
treef9e8bcbf17bca3853f088932d56a24588b2b13f7 /tuto0/_CoqProject
parent6617535fd1666a7010c6eb9a81b4405e9d4f9c8d (diff)
Port to coqpp.
Diffstat (limited to 'tuto0/_CoqProject')
-rw-r--r--tuto0/_CoqProject2
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
index dd93e1fa79..76368e3ac7 100644
--- a/tuto0/_CoqProject
+++ b/tuto0/_CoqProject
@@ -6,5 +6,5 @@ theories/Demo.v
src/tuto0_main.ml
src/tuto0_main.mli
-src/g_tuto0.ml4
+src/g_tuto0.mlg
src/tuto0_plugin.mlpack