From 661e782b0334cd448fd372a92bc8901b1654189a Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 11 Jan 2011 16:57:47 +0000
Subject: Add "Print Sorted Universes"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-ext.tex | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 7a56426c40..942530c3b7 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
-- 
cgit v1.2.3