diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /doc/refman/RefMan-ext.tex | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
-rw-r--r-- | doc/refman/RefMan-ext.tex | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 37660aa3..e0acef55 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -980,7 +980,7 @@ argument, use command Conversely, use command {\tt Unset Contextual Implicit} to unset the contextual implicit mode. -\subsection{Explicit Applications +\subsection{Explicit applications \index{Explicitation of implicit arguments} \label{Implicits-explicitation} \index{qualid@{\qualid}}} @@ -1208,6 +1208,35 @@ printing features, use the command {\tt Unset Printing All.} \end{quote} +\section{Printing universes} +\label{PrintingUniverses} +\comindex{Set Printing Universes} +\comindex{Unset Printing Universes} + +The following command: +\begin{quote} +{\tt Set Printing Universes} +\end{quote} +activates the display of the actual level of each occurrence of +{\Type}. See section~\ref{Sorts} for details. This wizard option, in +combination with \texttt{Set Printing All} (see +section~\ref{SetPrintingAll}) can help to diagnose failures to unify +terms apparently identical but internally different in the Calculus of +Inductive Constructions. To reactivate the display of the actual level +of the occurrences of {\Type}, use +\begin{quote} +{\tt Unset Printing Universes.} +\end{quote} + +\comindex{Print 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.} +\end{quote} + + %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |