diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 7a56426c4..942530c3b 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1750,16 +1750,20 @@ of the occurrences of {\Type}, use \end{quote} \comindex{Print Universes} +\comindex{Print Sorted Universes} The constraints on the internal level of the occurrences of {\Type} (see Section~\ref{Sorts}) can be printed using the command \begin{quote} -{\tt Print Universes.} +{\tt Print [Sorted] Universes.} \end{quote} +If the optional {\tt Sorted} option is given, each universe will be +made equivalent to a numbered label reflecting its level (with a +linear ordering) in the universe hierarchy. This command also accepts an optional output filename: \begin{quote} -\tt Print Universes {\str}. +\tt Print [Sorted] Universes {\str}. \end{quote} If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are printed in the DOT language, and can be processed by Graphviz |