Merge PR #9964: Unreleased changelog folder

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Reviewed-by: vbgl

27 files changed, 135 insertions, 68 deletions

diff --git a/.gitattributes b/.gitattributes
index 58b1a31d36..260e3f96b6 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -54,6 +54,7 @@ dune* whitespace=blank-at-eol,tab-in-indent
 .gitattributes whitespace=blank-at-eol,tab-in-indent
 _CoqProject whitespace=blank-at-eol,tab-in-indent
 Dockerfile whitespace=blank-at-eol,tab-in-indent
+00000-title.rst -whitespace
 
 # tabs are allowed in Makefiles.
 Makefile* whitespace=blank-at-eol
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/Makefile.doc b/Makefile.doc
index 23aa66a1b8..25d146000b 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -66,7 +66,7 @@ SPHINX_DEPS := coq
 endif
 
 # refman-html and refman-latex
-refman-%: $(SPHINX_DEPS)
+refman-%: $(SPHINX_DEPS) doc/unreleased.rst
 	$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
 	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \
 		$(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$*
@@ -116,6 +116,12 @@ plugin-tutorial: states tools
 doc/common/version.tex: config/Makefile
 	printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex
 
+### Changelog
+
+doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
+	$(SHOW)'AGGREGATE $@'
+	$(HIDE)cat doc/changelog/00-title.rst doc/changelog/*/*.rst > $@
+
 ######################################################################
 # Standard library
 ######################################################################
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/00-title.rst b/doc/changelog/00-title.rst
new file mode 100644
index 0000000000..628d9c8578
--- /dev/null
+++ b/doc/changelog/00-title.rst
@@ -0,0 +1,2 @@
+Unreleased changes
+------------------
diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst
new file mode 100644
index 0000000000..f680628a05
--- /dev/null
+++ b/doc/changelog/01-kernel/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Kernel**
+
diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst
new file mode 100644
index 0000000000..99bd2c5b44
--- /dev/null
+++ b/doc/changelog/02-specification-language/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Specification language, type inference**
+
diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst
new file mode 100644
index 0000000000..abc532df11
--- /dev/null
+++ b/doc/changelog/03-notations/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Notations**
+
diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst
new file mode 100644
index 0000000000..3c7802d632
--- /dev/null
+++ b/doc/changelog/04-tactics/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Tactics**
+
diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst
new file mode 100644
index 0000000000..06e9059b45
--- /dev/null
+++ b/doc/changelog/04-tactics/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/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst
new file mode 100644
index 0000000000..987b2a8ccd
--- /dev/null
+++ b/doc/changelog/04-tactics/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/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst
new file mode 100644
index 0000000000..b34d190298
--- /dev/null
+++ b/doc/changelog/05-tactic-language/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Tactic language**
+
diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst
new file mode 100644
index 0000000000..2e724627ec
--- /dev/null
+++ b/doc/changelog/06-ssreflect/00000-title.rst
@@ -0,0 +1,3 @@
+
+**SSReflect**
+
diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst
new file mode 100644
index 0000000000..3dfc45242d
--- /dev/null
+++ b/doc/changelog/06-ssreflect/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/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst
new file mode 100644
index 0000000000..1a0272983e
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Commands and options**
+
diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst
new file mode 100644
index 0000000000..bf462744fb
--- /dev/null
+++ b/doc/changelog/08-tools/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Tools**
+
diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst
new file mode 100644
index 0000000000..0fc27cf380
--- /dev/null
+++ b/doc/changelog/09-coqide/00000-title.rst
@@ -0,0 +1,3 @@
+
+**CoqIDE**
+
diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst
new file mode 100644
index 0000000000..d517a0e709
--- /dev/null
+++ b/doc/changelog/10-standard-library/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Standard library**
+
diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst
new file mode 100644
index 0000000000..732c088f45
--- /dev/null
+++ b/doc/changelog/10-standard-library/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/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst
new file mode 100644
index 0000000000..6b301f59d3
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Infrastructure and dependencies**
+
diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst
new file mode 100644
index 0000000000..5e709e2b27
--- /dev/null
+++ b/doc/changelog/12-misc/00000-title.rst
@@ -0,0 +1,3 @@
+
+**Miscellaneous**
+
diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst
new file mode 100644
index 0000000000..1113782180
--- /dev/null
+++ b/doc/changelog/12-misc/09964-changes.rst
@@ -0,0 +1,13 @@
+- Changelog has been moved from a specific file `CHANGES.md` to the
+  reference manual; former Credits chapter of the reference manual has
+  been split in two parts: a History chapter which was enriched with
+  additional historical information about Coq versions 1 to 5, and a
+  Changes chapter which was enriched with the content formerly in
+  `CHANGES.md` and `COMPATIBILITY`
+  (`#9133 <https://github.com/coq/coq/pull/9133>`_,
+  `#9668 <https://github.com/coq/coq/pull/9668>`_,
+  `#9939 <https://github.com/coq/coq/pull/9939>`_,
+  `#9964 <https://github.com/coq/coq/pull/9964>`_,
+  by Théo Zimmermann,
+  with help and ideas from Emilio Jesús Gallego Arias,
+  Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
new file mode 100644
index 0000000000..2891eb207e
--- /dev/null
+++ b/doc/changelog/README.md
@@ -0,0 +1,41 @@
+# 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 one of the sub-directories. 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..3a8efbb36d 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/00-title.rst 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
 ------------