9 files changed, 49 insertions, 36 deletions
diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst
new file mode 100644
index 0000000000..349c44c205
--- /dev/null
+++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst
@@ -0,0 +1,3 @@
+- Using ``SProp`` is now allowed by default, without needing to pass
+  ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811
+  <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
new file mode 100644
index 0000000000..580e808baa
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst
@@ -0,0 +1,7 @@
+- Update output generated by :flag:`Printing Dependent Evars Line` flag
+  used by the Prooftree tool in Proof General.
+  (`#10489 <https://github.com/coq/coq/pull/10489>`_,
+  closes `#4504 <https://github.com/coq/coq/issues/4504>`_,
+  `#10399 <https://github.com/coq/coq/issues/10399>`_ and
+  `#10400 <https://github.com/coq/coq/issues/10400>`_,
+  by Jim Fehrle).
diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
new file mode 100644
index 0000000000..6e87ff93c7
--- /dev/null
+++ b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
@@ -0,0 +1 @@
+- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin).
diff --git a/doc/changelog/README.md b/doc/changelog/README.md
index 2891eb207e..3e0970a656 100644
--- a/doc/changelog/README.md
+++ b/doc/changelog/README.md
@@ -7,25 +7,28 @@ 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.
+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
+Run `./dev/tools/make-changelog.sh`: it will ask you for your PR
+number, and to choose among the predefined categories.  Afterward,
+fill in the automatically generated entry with a short description of
+your change (which should describe any compatibility issues in
+particular).  You may also add a reference to the relevant fixed
+issue, and credit reviewers, co-authors, and anyone who helped advance
+the PR.
+
+The format for changelog entries is the same as in the reference
+manual.  In particular, 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:
+Here is a summary of the structure of a changelog entry:
 
 ``` rst
 - Description of the changes, with possible link to
@@ -35,7 +38,3 @@ The entry should be written using the following structure:
   [ 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/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 8935ba27e3..9a9ec78edc 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -9,15 +9,16 @@ SProp (proof irrelevant propositions)
 
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
-known as strict propositions). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
+known as strict propositions). Using :math:`\SProp` may be prevented
+by passing ``-disallow-sprop`` to the |Coq| program or using
+:flag:`Allow StrictProp`.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
 
    Allows using :math:`\SProp` when set and forbids it when unset. The
    initial value depends on whether you used the command line
-   ``-allow-sprop``.
+   ``-disallow-sprop`` and ``-allow-sprop``.
 
 .. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
    :undocumented:
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 0148925247..b6fcf9da22 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -198,21 +198,21 @@ Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2)
 with contributions from many users. A list of packages is available at
 https://coq.inria.fr/opam/www/.
 
-The 61 contributors to this version are David A. Dalrymple, Tanaka
-Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse
-Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric
-Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian
-Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj
-Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin,
-Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal
-Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee
-Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia
-Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume
-Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément
-Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan
-Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau,
-Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo
-Winterhalter, Beta Ziliani and Théo Zimmermann.
+The 61 contributors to this version are Tanaka Akira, Benjamin
+Barenblat, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Martin
+Bodin, Joachim Breitner, Tej Chajed, Frédéric Chapoton, Arthur
+Charguéraud, Cyril Cohen, Lukasz Czajka, David A. Dalrymple, Christian
+Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego
+Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross,
+Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi,
+Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier
+Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia
+Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez,
+Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot,
+Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Ryan Scott,
+Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, Enrico
+Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter,
+Xia Li-yao, Beta Ziliani and Théo Zimmermann.
 
 Many power users helped to improve the design of the new features via
 the issue and pull request system, the |Coq| development mailing list,
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 47ecfb9db0..9e219bd503 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -62,7 +62,7 @@ A simple example of a ``_CoqProject`` file follows:
     theories/foo.v
     theories/bar.v
     -I src/
-    src/baz.ml4
+    src/baz.mlg
     src/bazaux.ml
     src/qux_plugin.mlpack
 
@@ -111,7 +111,7 @@ decide how to build them. In particular:
 + |Coq| files must use the ``.v`` extension
 + |OCaml| files must use the ``.ml`` or ``.mli`` extension
 + |OCaml| files that require pre processing for syntax
-  extensions (like ``VERNAC EXTEND``) must use the ``.ml4`` extension
+  extensions (like ``VERNAC EXTEND``) must use the ``.mlg`` extension
 + In order to generate a plugin one has to list all |OCaml|
   modules (i.e. ``Baz`` for ``baz.ml``) in a ``.mlpack`` file (or ``.mllib``
   file).
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 2885d6dc33..843459b723 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1012,8 +1012,9 @@ Controlling display
 
 .. flag:: Printing Dependent Evars Line
 
-   This option controls the printing of the “(dependent evars: …)” line when
-   ``-emacs`` is passed.
+   This option controls the printing of the “(dependent evars: …)” information
+   after each tactic.  The information is used by the Prooftree tool in Proof
+   General. (https://askra.de/software/prooftree)
 
 
 .. _vernac-controlling-the-reduction-strategies:
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index d1b98b94a3..75c8c6c1ea 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -627,5 +627,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq88.v
     theories/Compat/Coq89.v
     theories/Compat/Coq810.v
+    theories/Compat/Coq811.v
   </dd>
 </dl>