6 files changed, 26 insertions, 18 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 795fccbf08..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
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 56f84d0ff0..b410833d25 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -194,14 +194,14 @@ Program Fixpoint
    The optional order annotation follows the grammar:
 
    .. productionlist:: orderannot
-      order      : measure `term` (`term`)? | wf `term` `term`
+      order      : measure `term` [ `term` ] | wf `term` `ident`
 
-   + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on
-     any subset of the arguments and the optional (parenthesised) term
-     ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R``
-     to ``lt``.
+   + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on
+     any subset of the arguments and the optional term
+     :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R`
+     to :g:`lt`.
 
-   + :g:`wf R x` which is equivalent to :g:`measure x (R)`.
+   + :g:`wf R x` which is equivalent to :g:`measure x R`.
 
    The structural fixpoint operator behaves just like the one of |Coq| (see
    :cmd:`Fixpoint`), except it may also generate obligations. It works
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/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 015b84c530..c0c8c2d79c 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -19,6 +19,9 @@ known as strict propositions). To use :math:`\SProp` you must pass
    initial value depends on whether you used the command line
    ``-allow-sprop``.
 
+.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
+   :undocumented:
+
 .. coqtop:: none
 
    Set Allow StrictProp.
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`.