Add "Print Sorted Universes"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7

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