Merge PR #9964: Unreleased changelog folder

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

21 files changed, 123 insertions, 0 deletions

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