10 files changed, 14 insertions, 14 deletions
diff --git a/.gitignore b/.gitignore
index 587a6191ab..ad5204847c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -135,7 +135,7 @@ ide/protocol/xml_lexer.ml
 coqpp/coqpp_parse.ml
 coqpp/coqpp_parse.mli
 
-# .ml4 / .mlp files
+# .mlg / .mlp files
 
 g_*.ml
 
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
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).
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index e0d63a723e..0a41bba8ce 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -597,7 +597,7 @@ let unfreeze (grams, lex) =
 (** No need to provide an init function : the grammar state is
     statically available, and already empty initially, while
     the lexer state should not be reset, since it contains
-    keywords declared in g_*.ml4 *)
+    keywords declared in g_*.mlg *)
 
 let parser_summary_tag =
   Summary.declare_summary_tag "GRAMMAR_LEXER"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 10f78a5a72..ca5adf8ab3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -108,7 +108,7 @@ end
 
     - "f" constr(x) (developer gives an EXTEND rule)
         |
-        | macro-generation in tacextend.ml4/vernacextend.ml4/argextend.ml4
+        | macro-generation in tacextend.mlg/vernacextend.mlg/argextend.mlg
         V
       [GramTerminal "f";
        GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")]
diff --git a/plugins/cc/README b/plugins/cc/README
index c616b5daab..7df7b971e8 100644
--- a/plugins/cc/README
+++ b/plugins/cc/README
@@ -9,7 +9,7 @@ Files :
 
 - ccalgo.ml : congruence closure algorithm
 - ccproof.ml : proof generation code
-- cctac.ml4 : the tactic itself
+- cctac.mlg : the tactic itself
 - CCSolve.v : a small Ltac tactic based on congruence 
 
 Known Bugs : the congruence tactic can fail due to type dependencies.
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index ef012e5092..f47a14cdc7 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (* This file uses the (non-compressed) union-find structure to generate *)
-(* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
+(* proof-trees that will be transformed into proof-terms in cctac.mlg   *)
 
 open CErrors
 open Constr
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index d37d2bea94..08253e5a8f 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -266,7 +266,7 @@ CMIFILES = \
 	$(CMOFILES:.cmo=.cmi) \
 	$(MLIFILES:.mli=.cmi)
 # the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
-# a .ml4 file
+# a .mlg file
 CMXSFILES = \
 	$(MLPACKFILES:.mlpack=.cmxs) \
 	$(CMXAFILES:.cmxa=.cmxs) \