diff options
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 942530c3b..62875be0d 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1755,7 +1755,7 @@ of the occurrences of {\Type}, use 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 [Sorted] Universes.} +{\tt Print \zeroone{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 @@ -1763,7 +1763,7 @@ linear ordering) in the universe hierarchy. This command also accepts an optional output filename: \begin{quote} -\tt Print [Sorted] Universes {\str}. +\tt Print \zeroone{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 |