New infrastructure for the unreleased changelog.

Move existing entries.

8 files changed, 73 insertions, 0 deletions

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
 ------------