2 files changed, 15 insertions, 1 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 22c75b4fc8..cab6739998 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -462,11 +462,18 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}.
 
 This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
 
+\subsection{\tt Set Typeclasses Axioms Are Instances}
+\optindex{Typeclasses Axioms Are Instances}
+
+This option (off by default since 8.8) automatically declares axioms
+whose type is a typeclass at declaration time as instances of that
+class.
+
 \subsection{\tt Set Typeclasses Dependency Order}
 \optindex{Typeclasses Dependency Order}
 
 This option (on by default since 8.6) respects the dependency order between
-subgoals, meaning that subgoals which are depended on by other subgoals 
+subgoals, meaning that subgoals which are depended on by other subgoals
 come first, while the non-dependent subgoals were put before the
 dependent ones previously (Coq v8.5 and below). This can result in quite
 different performance behaviors of proof search.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 60cd8b73a4..3ebeba178a 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -10,6 +10,8 @@ defined object referred by {\qualid}.
 
 \begin{ErrMsgs}
 \item {\qualid} \errindex{not a defined object}
+\item \errindex{Universe instance should have length} $n$.
+\item \errindex{This object does not support universe names.}
 \end{ErrMsgs}
 
 \begin{Variants}
@@ -27,6 +29,11 @@ constructor, abbreviation, \ldots), long name, type, implicit
 arguments and argument scopes. It does not print the body of
 definitions or proofs.
 
+\item {\tt Print {\qualid}@\{names\}.}\\
+This locally renames the polymorphic universes of {\qualid}.
+An underscore means the raw universe is printed.
+This form can be used with {\tt Print Term} and {\tt About}.
+
 %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
 %In case \qualid\ denotes an opaque theorem defined in a section,
 %it is stored on a special unprintable form and displayed as