Merge PR #1033: Universe binder improvements

1 files changed, 7 insertions, 0 deletions

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 60cd8b73a..3ebeba178 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