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

4 files changed, 50 insertions, 7 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"
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 81663bb918..3684074fde 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -488,9 +488,8 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
 	  VernacDeclareMLModule l
 
-      (* Dump of the universe graph - to file or to stdout *) 
       | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
-	  VernacPrint (PrintUniverses fopt)
+	  error "This command is deprecated, use Print Universes"
 
       | IDENT "Locate"; l = locatable -> VernacLocate l
 
@@ -626,7 +625,8 @@ GEXTEND Gram
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]  
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid
+      | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index a1ac9f1846..9d1d8d1846 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -67,9 +67,9 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
   | Invalid_argument s -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
   | Sys.Break -> 
-      hov 0 (fnl () ++ str "User Interrupt.")
+      hov 0 (fnl () ++ str "User interrupt.")
   | Univ.UniverseInconsistency -> 
-      hov 0 (str "Error: Universe Inconsistency.")
+      hov 0 (str "Error: Universe inconsistency.")
   | TypeError(ctx,te) -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
   | PretypeError(ctx,te) ->