New infrastructure for the unreleased changelog.

Move existing entries.

12 files changed, 77 insertions, 67 deletions

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 73b61ee0d9..3bd3342329 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.md.
+- [ ] Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).
diff --git a/CHANGES.md b/CHANGES.md
deleted file mode 100644
index 28ea84e4e3..0000000000
--- a/CHANGES.md
+++ /dev/null
@@ -1,63 +0,0 @@
-Unreleased changes
-==================
-
-<!-- Until https://github.com/coq/coq/pull/9964 is merged, we continue
-     adding changelog entry here. -->
-
-**Kernel**
-
-
-**Specification language, type inference**
-
-
-**Notations**
-
-
-**Tactics**
-
-- New variant change_no_check of change (usable as a documented
-  replacement of convert_concl_no_check).
-
-**Tactic language**
-
-- Modes are now taken into account by `typeclasses eauto` for local hypotheses.
-
-**SSReflect**
-
-- `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
-
-- New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
-  class, simplified `predType` interface: `pred_class` and `mkPredType`
-  deprecated, `{pred T}` and `PredType` should be used instead.
-
-- `if c return t then ...` now expects `c` to be a variable bound in `t`.
-
-- New `nonPropType` interface matching types that do _not_ have sort `Prop`.
-
-- New `relpre R f` definition for the preimage of a relation R under f.
-
-
-**Commands and options**
-
-
-**Tools**
-
-
-**CoqIDE**
-
-
-**Standard library**
-
-- Added Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull
-
-
-**Infrastructure and dependencies**
-
-
-**Miscellaneous**
-
-
-Released changes
-================
-
-See <https://coq.github.io/doc/master/refman/changes.html>.
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 4c5bd29236..ea9af60330 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1316,7 +1316,6 @@ 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.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/doc/MERGING.md b/dev/doc/MERGING.md
index 3f1b470878..c9eceb1270 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -71,8 +71,9 @@ 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.md`](../../CHANGES.md) or
-the [`dev/doc/changes.md`](changes.md) file.
+Moreover the PR author *must* add an entry to the [unreleased
+changelog](../../doc/changelog/README.md) or to the
+[`dev/doc/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.
diff --git a/doc/changelog/00000-title.rst b/doc/changelog/00000-title.rst
new file mode 100644
index 0000000000..628d9c8578
--- /dev/null
+++ b/doc/changelog/00000-title.rst
@@ -0,0 +1,2 @@
+Unreleased changes
+------------------
diff --git a/doc/changelog/09984-pairusualdecidabletypefull.rst b/doc/changelog/09984-pairusualdecidabletypefull.rst
new file mode 100644
index 0000000000..732c088f45
--- /dev/null
+++ b/doc/changelog/09984-pairusualdecidabletypefull.rst
@@ -0,0 +1,3 @@
+- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
+  (`#9984 <https://github.com/coq/coq/pull/9984>`_,
+  by Jean-Christophe Léchenet and Oliver Nash).
diff --git a/doc/changelog/09995-notations.rst b/doc/changelog/09995-notations.rst
new file mode 100644
index 0000000000..3dfc45242d
--- /dev/null
+++ b/doc/changelog/09995-notations.rst
@@ -0,0 +1,8 @@
+- `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
+  New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
+  class, simplified `predType` interface: `pred_class` and `mkPredType`
+  deprecated, `{pred T}` and `PredType` should be used instead.
+  `if c return t then ...` now expects `c` to be a variable bound in `t`.
+  New `nonPropType` interface matching types that do _not_ have sort `Prop`.
+  New `relpre R f` definition for the preimage of a relation R under f
+  (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier).
diff --git a/doc/changelog/09996-hint-mode.rst b/doc/changelog/09996-hint-mode.rst
new file mode 100644
index 0000000000..06e9059b45
--- /dev/null
+++ b/doc/changelog/09996-hint-mode.rst
@@ -0,0 +1,5 @@
+- Modes are now taken into account by :tacn:`typeclasses eauto` for
+  local hypotheses
+  (`#9996 <https://github.com/coq/coq/pull/9996>`_,
+  fixes `#5752 <https://github.com/coq/coq/issues/5752>`_,
+  by Maxime Dénès, review by Pierre-Marie Pédrot).
diff --git a/doc/changelog/10059-change-no-check.rst b/doc/changelog/10059-change-no-check.rst
new file mode 100644
index 0000000000..987b2a8ccd
--- /dev/null
+++ b/doc/changelog/10059-change-no-check.rst
@@ -0,0 +1,7 @@
+- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
+  documented replacement of :tacn:`convert_concl_no_check`
+  (`#10012 <https://github.com/coq/coq/pull/10012>`_,
+  `#10017 <https://github.com/coq/coq/pull/10017>`_,
+  `#10053 <https://github.com/coq/coq/pull/10053>`_, and
+  `#10059 <https://github.com/coq/coq/pull/10059>`_,
+  by Hugo Herbelin and Paolo G. Giarrusso).
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
new file mode 100644
index 0000000000..64359e45ba
--- /dev/null
+++ b/doc/changelog/README.md
@@ -0,0 +1,40 @@
+# Unreleased changelog #
+
+## When to add an entry? ##
+
+All new features, user-visible changes to features, user-visible or
+otherwise important infrastructure changes, and important bug fixes
+should get a changelog entry.
+
+Compatibility-breaking changes should always get a changelog entry,
+which should explain what compatibility-breakage is to expect.
+
+Pull requests changing the ML API in significant ways should add an
+entry in [`dev/doc/changes.md`](../../dev/doc/changes.md).
+
+## How to add an entry? ##
+
+You should create a file in this folder. The name of the file should
+be `NNNNN-identifier.rst` where `NNNNN` is the number of the pull
+request on five digits and `identifier` is whatever you want.
+
+This file should use the same format as the reference manual (as it
+will be copied in there). You may reference the documentation you just
+added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See
+the [documentation of the Sphinx format](../sphinx/README.rst) of the
+manual for details.
+
+The entry should be written using the following structure:
+
+``` rst
+- Description of the changes, with possible link to
+  :ref:`relevant-section` of the updated documentation
+  (`#PRNUM <https://github.com/coq/coq/pull/PRNUM>`_,
+  [fixes `#ISSUE1 <https://github.com/coq/coq/issues/ISSUE1>`_
+  [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],]
+  by Full Name[, with help / review of Full Name]).
+```
+
+The description should be kept rather short and the only additional
+required meta-information are the link to the pull request and the
+full name of the author.
diff --git a/doc/dune b/doc/dune
index bd40104725..06f78013aa 100644
--- a/doc/dune
+++ b/doc/dune
@@ -11,6 +11,7 @@
   (package coq)
   (source_tree sphinx)
   (source_tree tools)
+  unreleased.rst
   (env_var SPHINXWARNOPT))
  (action
   (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html)))
@@ -19,6 +20,11 @@
  (name refman-html)
  (deps sphinx_build))
 
+(rule
+ (targets unreleased.rst)
+ (deps (source_tree changelog))
+ (action (with-stdout-to %{targets} (bash "cat changelog/*.rst"))))
+
 ; The install target still needs more work.
 ; (install
 ;  (section doc)
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 1c4c748295..5704587ae0 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -2,6 +2,8 @@
 Recent changes
 --------------
 
+.. include:: ../unreleased.rst
+
 Version 8.10
 ------------