Rename CHANGES to CHANGES.md.

7 files changed, 8 insertions, 8 deletions

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 4a8606a38a..73b61ee0d9 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -16,4 +16,4 @@ Fixes / closes #????
 <!-- If this is a feature pull request / breaks compatibility: -->
 <!-- (Otherwise, remove these lines.) -->
 - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
-- [ ] Entry added in CHANGES.
+- [ ] Entry added in CHANGES.md.
diff --git a/CHANGES b/CHANGES.md
index 2f31ab1950..2f31ab1950 100644
--- a/CHANGES
+++ b/CHANGES.md
diff --git a/README.md b/README.md
index fcf20f0097..e6a52e95e3 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ),
 for additional user-contributed documentation.
 
 ## Changes
-There is a file named [`CHANGES`](CHANGES) that explains the differences and the
+There is a file named [`CHANGES.md`](CHANGES.md) that explains the differences and the
 incompatibilities since last versions. If you upgrade Coq, please read
 it carefully.
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 5f07aa8fca..b8bea755e0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1374,7 +1374,7 @@ function copy_coq_license {
     # FIXME: this is not the micromega license
     # It only applies to code that was copied into one single file!
     install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D CHANGES                        "$PREFIXCOQ/license_readme/coq/Changes.txt"
+    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 24952eb5b7..7870cbb51d 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    developer who merges the PR on Coq. There are plans to improve this, cf.
    [#6724](https://github.com/coq/coq/issues/6724).
 
-Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 Advanced GitLab CI information
 ------------------------------
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index c0cd9c8cdd..000f21c254 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -54,7 +54,7 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
@@ -93,7 +93,7 @@ When the PR has conflicts, the assignee can either:
 
 In both cases, CI should be run again.
 
-In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix
 the conflicts in the merge commit (following the same steps as below), and push
 to `master` directly. Don't use the GitHub interface to fix these conflicts.
 
diff --git a/doc/sphinx/credits-contents.rst b/doc/sphinx/credits-contents.rst
index 212f0a65b0..d1df0657aa 100644
--- a/doc/sphinx/credits-contents.rst
+++ b/doc/sphinx/credits-contents.rst
@@ -1238,7 +1238,7 @@ of integers and real constants are now represented using `IZR` (work by
 Guillaume Melquiond).
 
 Standard library additions and improvements by Jason Gross, Pierre Letouzey and
-others, documented in the `CHANGES` file.
+others, documented in the ``CHANGES.md`` file.
 
 The mathematical proof language/declarative mode plugin was removed from the
 archive.
@@ -1352,7 +1352,7 @@ version.
 
 Version 8.8 also comes with a bunch of smaller-scale changes and
 improvements regarding the different components of the system.
-Most important ones are documented in the ``CHANGES`` file.
+Most important ones are documented in the ``CHANGES.md`` file.
 
 The efficiency of the whole system has seen improvements thanks to
 contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and