Merge remote-tracking branch 'origin/master' into stm+doc_hook

16 files changed, 89 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/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
new file mode 100644
index 0000000000..0a902079b9
--- /dev/null
+++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
@@ -0,0 +1,4 @@
+- Record fields can be annotated to prevent them from being used as canonical projections;
+  see :ref:`canonicalstructures` for details
+  (`#10076 <https://github.com/coq/coq/pull/10076>`_,
+  by Vincent Laporte).
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/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/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/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
new file mode 100644
index 0000000000..78874cadb1
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst
@@ -0,0 +1,6 @@
+- Deprecated flag `Refine Instance Mode` has been removed.
+  (`#09530 <https://github.com/coq/coq/pull/09530>`_, fixes
+  `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890
+  <https://github.com/coq/coq/issues/3890>`_ and `#4638
+  <https://github.com/coq/coq/issues/4638>`_
+  by Maxime Dénès, review by Gaëtan Gilbert).
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/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/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.