4 files changed, 29 insertions, 8 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index b568160356..45b3f6f161 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -192,7 +192,7 @@ Disjunctive patterns
 --------------------
 
 Multiple patterns that share the same right-hand-side can be
-factorized using the notation :n:`{+| @mult_pattern}`. For
+factorized using the notation :n:`{+| @patterns_comma}`. For
 instance, :g:`max` can be rewritten as follows:
 
 .. coqtop:: in reset
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 9f92fc4c56..7136cc28d1 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -283,7 +283,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an
 arity, that is a sequence of product finished by a sort), then some type
 variables have to be given (as quoted strings). The syntax is then:
 
-.. cmdv:: Extract Constant @qualid @string ... @string => @string
+.. cmdv:: Extract Constant @qualid {+ @string } => @string
    :undocumented:
 
 The number of type variables is checked by the system. For example:
@@ -530,7 +530,7 @@ A detailed example: Euclidean division
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The file ``Euclid`` contains the proof of Euclidean division.
-The natural numbers used here are unary, represented by the type``nat``,
+The natural numbers used here are unary, represented by the type ``nat``,
 which is defined by two constructors ``O`` and ``S``.
 This module contains a theorem ``eucl_dev``, whose type is::
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index 93a1be027c..ca5b5e54a7 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -117,7 +117,7 @@ parameters is any term :math:`f \, t_1 \ldots t_n`.
 .. example:: Morphisms
 
    Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A``
-   perform the union of two sets by appending one list to the other. ``union` is a binary
+   perform the union of two sets by appending one list to the other. ``union`` is a binary
    morphism parametric over ``A`` that respects the relation instance
    ``(set_eq A)``. The latter condition is proved by showing:
 
@@ -741,7 +741,7 @@ following grammar:
             : topdown `strategy`         (top-down)
             : hints `ident`              (apply hints from hint database)
             : terms `term` ... `term`      (any of the terms)
-            : eval `redexpr`             (apply reduction)
+            : eval `red_expr`             (apply reduction)
             : fold `term`               (unify)
             : ( `strategy` )
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 1bbf988505..661aa88082 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -47,9 +47,22 @@ Leibniz equality on some type. An example implementation is:
          | tt, tt => eq_refl tt
          end }.
 
-Using :cmd:`Program Instance`, if one does not give all the members in
-the Instance declaration, Coq generates obligations for the remaining
-fields, e.g.:
+Using the attribute ``refine``, if the term is not sufficient to
+finish the definition (e.g. due to a missing field or non-inferable
+hole) it must be finished in proof mode. If it is sufficient a trivial
+proof mode with no open goals is started.
+
+.. coqtop:: in
+
+   #[refine] Instance unit_EqDec' : EqDec unit := { eqb x y := true }.
+   Proof. intros [] [];reflexivity. Defined.
+
+Note that if you finish the proof with :cmd:`Qed` the entire instance
+will be opaque, including the fields given in the initial term.
+
+Alternatively, in :flag:`Program Mode` if one does not give all the
+members in the Instance declaration, Coq generates obligations for the
+remaining fields, e.g.:
 
 .. coqtop:: in
 
@@ -563,6 +576,14 @@ Settings
    of goals.  Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this
    option to 0 turns that flag off.
 
+.. flag:: Typeclasses Axioms Are Instances
+
+   .. deprecated:: 8.10
+
+   This flag (off by default since 8.8) automatically declares axioms
+   whose type is a typeclass at declaration time as instances of that
+   class.
+
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~