diff options
| author | glondu | 2011-01-12 10:25:03 +0000 |
|---|---|---|
| committer | glondu | 2011-01-12 10:25:03 +0000 |
| commit | c7c3fd68b065bcdee45585b2241c91360223b249 (patch) | |
| tree | f4be57b8ff580cc4605f7f6a268b58ddaa34c0ed | |
| parent | 323edea04a7af5f3fa7745cef5130362f494354a (diff) | |
Fix formatting issue in refman
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13791 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 942530c3b7..62875be0d0 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 |