9 files changed, 45 insertions, 29 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index a9d894cab5..dd21ea09bd 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -92,7 +92,7 @@ and use the ``==`` notation on terms of this type.
 Derived Canonical Structures
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-We know how to use ``== `` on base types, like ``nat``, ``bool``, ``Z``. Here we show
+We know how to use ``==`` on base types, like ``nat``, ``bool``, ``Z``. Here we show
 how to deal with type constructors, i.e. how to make the following
 example work:
 
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index d15aacad44..d5523e8561 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -154,8 +154,10 @@ Declaring Coercions
   .. warn:: Ambiguous path.
 
      When the coercion :token:`qualid` is added to the inheritance graph,
-     invalid coercion paths are ignored; they are signaled by a warning
-     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+     invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check
+     that they are convertible with existing ones on the same classes.
+     The paths for which this check fails are displayed by a warning in the form
+     :g:`[f₁;..;fₙ] : C >-> D`.
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
@@ -322,21 +324,8 @@ are also forgotten.
 Coercions and Modules
 ---------------------
 
-.. flag:: Automatic Coercions Import
-
-   Since |Coq| version 8.3, the coercions present in a module are activated
-   only when the module is explicitly imported. Formerly, the coercions
-   were activated as soon as the module was required, whether it was
-   imported or not.
-
-   This option makes it possible to recover the behavior of the versions of
-   |Coq| prior to 8.3.
-
-.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
-
-   This warning is emitted when typechecking relies on a coercion
-   contained in a module that has not been explicitely imported. It helps
-   migrating code and stop relying on the option above.
+The coercions present in a module are activated only when the module is
+explicitly imported.
 
 Examples
 --------
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 20e4c6a3d6..3b350d5dc0 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -323,7 +323,7 @@ The syntax for adding a new ring is
    decidable :n:`@term`
       declares the ring as computational. The expression
       :n:`@term` is the correctness proof of an equality test ``?=!``
-      (which  hould be evaluable). Its type should be of the form
+      (which should be evaluable). Its type should be of the form
       ``forall x y, x ?=! y = true → x == y``.
 
    morphism :n:`@term`
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index e6a5b3972c..b069cf27f4 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -561,6 +561,8 @@ Settings
 
 .. flag:: Refine Instance Mode
 
+   .. deprecated:: 8.10
+
    This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
@@ -573,18 +575,19 @@ Settings
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth
+.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num
    :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass
    resolution tactic. The semantics of the options are:
 
-   + ``debug`` In debug mode, the trace of successfully applied tactics is
-     printed.  This value can also be set with :flag:`Typeclasses Debug`.
+   + ``debug`` This sets the debug mode. In debug mode, the trace of
+     successfully applied tactics is printed. The debug mode can also
+     be set with :flag:`Typeclasses Debug`.
 
-   + ``dfs, bfs`` This sets the search strategy to depth-first search (the
-     default) or breadth-first search.  This value can also be set with
-     :flag:`Typeclasses Iterative Deepening`.
+   + ``(dfs)``, ``(bfs)`` This sets the search strategy to depth-first
+     search (the default) or breadth-first search. The search strategy
+     can also be set with :flag:`Typeclasses Iterative Deepening`.
 
-   + ``depth`` This sets the depth limit of the search.  This value can also be set with
-     :opt:`Typeclasses Depth`.
+   + :token:`num` This sets the depth limit of the search. The depth
+     limit can also be set with :opt:`Typeclasses Depth`.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 18cafd1f21..695dea222f 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1430,8 +1430,8 @@ with the same physical-to-logical translation and with an empty logical prefix.
 The command line option ``-R`` is a variant of ``-Q`` which has the strictly
 same behavior regarding loadpaths, but which also makes the
 corresponding ``.vo`` files available through their short names in a way
-not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib``
-associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name
+not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R path Lib``
+associates to the file ``/path/fOO/Bar/File.vo`` the logical name
 ``Lib.fOO.Bar.File``, but allows this file to be accessed through the
 short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with
 identical base name are present in different subdirectories of a
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 52e3029b8f..0322b43694 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1071,6 +1071,16 @@ Proving a subgoal as a separate lemma
    It may be useful to generate lemmas minimal w.r.t. the assumptions they
    depend on. This can be obtained thanks to the option below.
 
+   .. warning::
+
+      The abstract tactic, while very useful, still has some known
+      limitations, see https://github.com/coq/coq/issues/9146 for more
+      details. Thus we recommend using it caution in some
+      "non-standard" contexts. In particular, ``abstract`` won't
+      properly work when used inside quotations ``ltac:(...)``, or
+      if used as part of typeclass resolution, it may produce wrong
+      terms when in universe polymorphic mode.
+
    .. tacv:: abstract @expr using @ident
 
       Give explicitly the name of the auxiliary lemma.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 07215a0c7e..16b158c397 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -544,6 +544,10 @@ Requesting information
 
       ``<Your Tactic Text here>``.
 
+     .. deprecated:: 8.10
+
+        Please use a text editor.
+
    .. cmdv:: Show Proof
       :name: Show Proof
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7b395900e9..afb0239be4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3912,6 +3912,8 @@ At Coq startup, only the core database is nonempty and can be used.
                       environment, including those used for ``setoid_rewrite``,
                       from the Classes directory.
 
+:fset: internal database for the implementation of the ``FSets`` library.
+
 You are advised not to put your own hints in the core database, but
 use one or several databases specific to your development.
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index e5eb7eb4f5..1e201953b3 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1473,6 +1473,10 @@ Numeral notations
      :n:`@ident__2` to the number will be fully reduced, and universes
      of the resulting term will be refreshed.
 
+     Note that only fully-reduced ground terms (terms containing only
+     function application, constructors, inductive type families, and
+     primitive integers) will be considered for printing.
+
    .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
 
      When a literal larger than :token:`num` is parsed, a warning
@@ -1618,6 +1622,10 @@ String notations
      :n:`@ident__2` to the string will be fully reduced, and universes
      of the resulting term will be refreshed.
 
+     Note that only fully-reduced ground terms (terms containing only
+     function application, constructors, inductive type families, and
+     primitive integers) will be considered for printing.
+
    .. exn:: Cannot interpret this string as a value of type @type
 
      The string notation registered for :token:`type` does not support