3 files changed, 19 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 56d90b33d8..2474c784b8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -391,6 +391,16 @@ Summary of the commands
       equivalent to ``Hint Resolve ident : typeclass_instances``, except it
       registers instances for :cmd:`Print Instances`.
 
+   .. flag:: Instance Generalized Output
+
+      .. deprecated:: 8.13
+
+      Disabled by default, this provides compatibility with Coq
+      version 8.12 and earlier.
+
+      When enabled, the type of the instance is implicitly generalized
+      over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``.
+
 .. cmd:: Print Instances @reference
 
    Shows the list of instances associated with the typeclass :token:`reference`.
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index e6dc6f6c51..485b92342d 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -280,9 +280,7 @@ automatically created.
      sections.
 
    + :attr:`export` are visible from other modules when they import the current
-     module. Requiring it is not enough. This attribute is only effective for
-     the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and
-     :cmd:`Hint Extern` variants of the command.
+     module. Requiring it is not enough.
 
    + :attr:`global` hints are made available by merely requiring the current
      module.
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index 7ab8f9d763..b68b2ed2a7 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -200,6 +200,14 @@ at the beginning of a line.
           if n <= 1 then 1 else n * fact (n-1)
       >>
 
+Verbatim material on a single line is also possible (assuming that
+``>>`` is not part of the text to be presented as verbatim).
+
+.. example::
+
+  ::
+
+      Here is the corresponding caml expression: << fact (n-1) >>
 
 
 Hyperlinks