Doc update with mlg extension - fix #10855

3 files changed, 6 insertions, 6 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/.
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 601d52ddda..2f5c7128e2 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -727,7 +727,7 @@ Conflicts exists between integers and constrs.
 \nlsep \TERM{setoid_replace} ~\tacconstr ~\KWD{with} ~\tacconstr
 \nlsep \TERM{setoid_rewrite} ~\NT{orient} ~\tacconstr
 \nlsep \TERM{subst} ~\STAR{\NT{ident}}
-%% eqdecide.ml4
+%% eqdecide.mlg
 \nlsep \TERM{decide}~\TERM{equality} ~\OPTGR{\tacconstr~\tacconstr}
 \nlsep \TERM{compare}~\tacconstr~\tacconstr
 %% eauto