From 3e0bf68bdc1ac6bde7bd04236657fb4d554817ad Mon Sep 17 00:00:00 2001
From: mcaci
Date: Sat, 12 Oct 2019 14:24:18 +0200
Subject: Doc update with mlg extension - fix #10855

---
 doc/sphinx/practical-tools/utilities.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 47ecfb9db0..9e219bd503 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows:
     theories/foo.v
     theories/bar.v
     -I src/
-    src/baz.ml4
+    src/baz.mlg
     src/bazaux.ml
     src/qux_plugin.mlpack
 
@@ -111,7 +111,7 @@ decide how to build them. In particular:
 + |Coq| files must use the ``.v`` extension
 + |OCaml| files must use the ``.ml`` or ``.mli`` extension
 + |OCaml| files that require pre processing for syntax
-  extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension
+  extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension
 + In order to generate a plugin one has to list all |OCaml|
   modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib``
   file).
-- 
cgit v1.2.3