Documentation de "Set Printing Universes", "Print Universes" (anciennement

"Dump Universes"), "Universe inconsistency", et description brève des univers 
algébriques.


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

2 files changed, 45 insertions, 2 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index a79f9d2b68..34b5a3fbf9 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -118,7 +118,21 @@ indexes can be solved. From the user point of view we consequently
 have {\sf Type :Type}.
 
 We shall make precise in the typing rules the constraints between the
-indexes.
+indexes. 
+
+\paragraph{Implementation issues}
+In practice, the {\Type} hierarchy is implemented using algebraic
+universes. An algebraic universe $u$ is either a variable (a qualified
+identifier with a number) or a successor of an algebraic universe (an
+expression $u+1$), or an upper bound of algebraic universes (an
+expression $max(u_1,...,u_n)$), or the base universe (the expression
+$0$) which corresponds, in the arity of sort-polymorphic inductive
+types, to the predicative sort {\Set}. A graph of constraints between
+the universe variables is maintained globally. To ensure the existence
+of a mapping of the universes to the positive integers, the graph of
+constraints must remain acyclic.  Typing expressions that violate the
+acyclicity of the graph of constraints results in a \errindex{Universe
+inconsistency} error (see also section~\ref{PrintingUniverses}).
 
 \subsection{Constants}
 Besides the sorts, the language also contains constants denoting
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 37660aa3a7..e0acef5503 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"