Doc update with mlg extension - fix #10855

2 files changed, 5 insertions, 5 deletions

diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index a14781a058..b8987b7086 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -89,7 +89,7 @@ enables partial recalculation of dependencies (only the dependencies
 of changed files are recomputed).
 
 If you add a dependency to a Coq camlp5 extension (grammar.cma or
-q_constr.cmo), then see sections ".ml4 files" and "new files".
+q_constr.cmo), then see sections ".mlg files" and "new files".
 
 Cleaning Targets
 ----------------
@@ -113,13 +113,13 @@ Targets for cleaning various parts:
 
  - docclean: clean documentation
 
-.ml4/.mlp files
+.mlg/.mlp files
 ---------------
 
 There is now two kinds of preprocessed files : 
  - a .mlp do not need grammar.cma (they are in grammar/)
- - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
-   except coqide_main.ml4 and its specific rule
+ - a .mlg is now always preprocessed with grammar.cma (and q_constr.cmo),
+   except coqide_main.mlg and its specific rule
 
 This classification replaces the old mechanism of declaring the use
 of a grammar extension via a line of the form:
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index e5e4f740bd..096ffe6a1c 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -20,7 +20,7 @@ Special components
 grammar :
 
  Camlp5 syntax extensions. The file grammar/grammar.cma is used
- to pre-process .ml4 files containing EXTEND constructions,
+ to pre-process .mlg files containing EXTEND constructions,
  either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
  This grammar.cma incorporates many files from other directories
  (mainly parsing/), plus some specific files in grammar/.