4 files changed, 50 insertions, 14 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index b6fcf9da22..80a24b997c 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -726,6 +726,45 @@ Changes in 8.10.0
   fixes `#9512 <https://github.com/coq/coq/issues/9512>`_
   by Vincent Laporte).
 
+Changes in 8.10.1
+~~~~~~~~~~~~~~~~~
+
+A few bug fixes and documentation improvements, in particular:
+
+**Kernel**
+
+- Fix proof of False when using |SProp| (incorrect De Bruijn handling
+  when inferring the relevance mark of a function) (`#10904
+  <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot).
+
+**Tactics**
+
+- Fix an anomaly when unsolved evar in :cmd:`Add Ring`
+  (`#10891 <https://github.com/coq/coq/pull/10891>`_,
+  fixes `#9851 <https://github.com/coq/coq/issues/9851>`_,
+  by Gaëtan Gilbert).
+
+**Tactic language**
+
+- Fix Ltac regression in binding free names in uconstr
+  (`#10899 <https://github.com/coq/coq/pull/10899>`_,
+  fixes `#10894 <https://github.com/coq/coq/issues/10894>`_,
+  by Hugo Herbelin).
+
+**CoqIDE**
+
+- Fix handling of unicode input before space
+  (`#10852 <https://github.com/coq/coq/pull/10852>`_,
+  fixes `#10842 <https://github.com/coq/coq/issues/10842>`_,
+  by Arthur Charguéraud).
+
+**Extraction**
+
+- Fix custom extraction of inductives to JSON
+  (`#10897 <https://github.com/coq/coq/pull/10897>`_,
+  fixes `#4741 <https://github.com/coq/coq/issues/4741>`_,
+  by Helge Bahmann).
+
 Version 8.9
 -----------
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 03b30d5d97..57a54bc0ad 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -538,13 +538,11 @@ Requesting information
    .. cmdv:: Show Proof
       :name: Show Proof
 
-      It displays the proof term generated by the tactics
-      that have been applied. If the proof is not completed, this term
-      contain holes, which correspond to the sub-terms which are still to be
-      constructed. These holes appear as a question mark indexed by an
-      integer, and applied to the list of variables in the context, since it
-      may depend on them. The types obtained by abstracting away the context
-      from the type of each placeholder are also printed.
+      Displays the proof term generated by the tactics
+      that have been applied so far. If the proof is incomplete, the term
+      will contain holes, which correspond to subterms which are still to be
+      constructed. Each hole is an existential variable, which appears as a
+      question mark followed by an identifier.
 
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
@@ -574,9 +572,8 @@ Requesting information
    .. cmdv:: Show Existentials
       :name: Show Existentials
 
-      It displays the set of all uninstantiated
-      existential variables in the current proof tree, along with the type
-      and the context of each variable.
+      Displays all open goals / existential variables in the current proof
+      along with the type and the context of each variable.
 
    .. cmdv:: Show Match @ident
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 1d08001e34..75897fec45 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2670,7 +2670,7 @@ context entry name.
      Lemma test n m (H : m + 1 < n) : True.
      have @i : 'I_n by apply: (Sub m); omega.
 
-Note that the sub-term produced by :tacn:`omega` is in general huge and
+Note that the subterm produced by :tacn:`omega` is in general huge and
 uninteresting, and hence one may want to hide it.
 For this purpose the ``[: name ]`` intro pattern and the tactic
 ``abstract`` (see :ref:`abstract_ssr`) are provided.
@@ -4583,7 +4583,7 @@ The ``elim/`` tactic distinguishes two cases:
   passed to the eliminator as the last argument (``x`` in ``foo_ind``) and
   ``en−1 … e1`` are used as patterns to select in the goal the occurrences that
   will be bound by the predicate ``P``, thus it must be possible to unify
-  the sub-term of the goal matched by ``en−1`` with ``pm`` , the one matched
+  the subterm of the goal matched by ``en−1`` with ``pm`` , the one matched
   by ``en−2`` with ``pm−1`` and so on.
 :regular eliminator: in all the other cases. Here it must be possible
   to unify the term matched by ``en`` with ``pm`` , the one matched by
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index bcc5e914ac..a28ce600ca 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -750,12 +750,12 @@ level is otherwise given explicitly by using the syntax
 
 Levels are cumulative: a notation at level ``n`` of which the left end
 is a term shall use rules at level less than ``n`` to parse this
-sub-term. More precisely, it shall use rules at level strictly less
+subterm. More precisely, it shall use rules at level strictly less
 than ``n`` if the rule is declared with ``right associativity`` and
 rules at level less or equal than ``n`` if the rule is declared with
 ``left associativity``. Similarly, a notation at level ``n`` of which
 the right end is a term shall use by default rules at level strictly
-less than ``n`` to parse this sub-term if the rule is declared left
+less than ``n`` to parse this subterm if the rule is declared left
 associative and rules at level less or equal than ``n`` if the rule is
 declared right associative. This is what happens for instance in the
 rule