Univs: update refman, better printers for universe contexts.

4 files changed, 77 insertions, 53 deletions

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index cd8222269..f47973601 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -7,9 +7,7 @@
 \asection{General Presentation}
 
 \begin{flushleft}
-  \em The status of Universe Polymorphism is experimental. Some features
-  are not compatible with it (yet): bytecode compilation does not handle
-  polymorphic definitions, it treats them as opaque constants.
+  \em The status of Universe Polymorphism is experimental.
 \end{flushleft}
 
 This section describes the universe polymorphic extension of Coq.
@@ -65,7 +63,7 @@ Now \texttt{pidentity} is used at two different levels: at the head of
 the application it is instantiated at \texttt{Top.3} while in the
 argument position it is instantiated at \texttt{Top.4}. This definition
 is only valid as long as \texttt{Top.4} is strictly smaller than
-\texttt{Top.3}, as show by the constraints. Not that this definition is
+\texttt{Top.3}, as show by the constraints. Note that this definition is
 monomorphic (not universe polymorphic), so in turn the two universes are
 actually global levels.
 
@@ -119,18 +117,28 @@ producing global universe constraints, one can use the
 \begin{itemize}
 \item \texttt{Lemma}, \texttt{Axiom}, and all the other ``definition''
   keywords support polymorphism.
-\item \texttt{Variables}, \texttt{Context} in a section support polymorphism.
-  This means that the
-  variables are discharged polymorphically over definitions that use
-  them. In other words, two definitions in the section sharing a common
-  variable will both get parameterized by the universes produced by the 
-  variable declaration. This is in contrast to a ``mononorphic'' variable
-  which introduces global universes, making the two definitions depend on
-  the \emph{same} global universes associated to the variable.
+\item \texttt{Variables}, \texttt{Context}, \texttt{Universe} and
+  \texttt{Constraint} in a section support polymorphism.  This means
+  that the universe variables (and associated constraints) are
+  discharged polymorphically over definitions that use them. In other
+  words, two definitions in the section sharing a common variable will
+  both get parameterized by the universes produced by the variable
+  declaration. This is in contrast to a ``mononorphic'' variable which
+  introduces global universes and constraints, making the two
+  definitions depend on the \emph{same} global universes associated to
+  the variable.
 \item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint
   polymorphically, not at a single instance.
 \end{itemize}
 
+\asection{Global and local universes}
+
+Each universe is declared in a global or local environment before it can
+be used. To ensure compatibility, every \emph{global} universe is set to
+be strictly greater than \Set~when it is introduced, while every
+\emph{local} (i.e. polymorphically quantified) universe is introduced as
+greater or equal to \Set.
+
 \asection{Conversion and unification}
 
 The semantics of conversion and unification have to be modified a little
@@ -173,23 +181,48 @@ This definition is elaborated by minimizing the universe of id to level
 generated at the application of id and a constraint that $\Set \le i$.
 This minimization process is applied only to fresh universe
 variables. It simply adds an equation between the variable and its lower
-bound if it is an atomic universe (i.e. not an algebraic max()).
+bound if it is an atomic universe (i.e. not an algebraic \texttt{max()}
+universe).
 
-\asection{Explicit Universes}
+The option \texttt{Unset Universe Minimization ToSet} disallows
+minimization to the sort $\Set$ and only collapses floating universes
+between themselves.
 
-\begin{flushleft}
-  \em The design and implementation of explicit universes is very
-  experimental and is likely to change in future versions.
-\end{flushleft}
+\asection{Explicit Universes}
 
 The syntax has been extended to allow users to explicitly bind names to
-universes and explicitly instantiate polymorphic
-definitions. Currently, binding is implicit at the first occurrence of a 
-universe name. For example, i and j below are introduced by the
-annotations attached to Types. 
+universes and explicitly instantiate polymorphic definitions.
+
+\subsection{\tt Universe {\ident}.
+  \comindex{Universe}
+  \label{UniverseCmd}}
+
+In the monorphic case, this command declare a new global universe named
+{\ident}. It supports the polymorphic flag only in sections, meaning the
+universe quantification will be discharged on each section definition
+independently.
+
+\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
+  \comindex{Constraint}
+  \label{ConstraintCmd}}
+
+This command declare a new constraint between named universes. 
+The order relation can be one of $<$, $\le$ or $=$. If consistent, 
+the constraint is then enforced in the global environment. Like
+\texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix
+in sections only to declare constraints discharged at section closing time.
+
+\begin{ErrMsgs}
+\item \errindex{Undeclared universe {\ident}}.
+\item \errindex{Universe inconsistency}
+\end{ErrMsgs}
+
+\subsection{Polymorphic definitions}
+For polymorphic definitions, the declaration of (all) universe levels
+introduced by a definition uses the following syntax:
 
 \begin{coq_example*}
-Polymorphic Definition le (A : Type@{i}) : Type@{j} := A.
+Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A.
 \end{coq_example*}
 \begin{coq_example}
 Print le.
@@ -197,40 +230,32 @@ Print le.
 
 During refinement we find that $j$ must be larger or equal than $i$, as
 we are using $A : Type@{i} <= Type@{j}$, hence the generated
-constraint. Note that the names here are not bound in the final
-definition, they just allow to specify locally what relations should
-hold. In the term and in general in proof mode, universe names
-introduced in the types can be referred to in terms.
+constraint. At the end of a definition or proof, we check that the only
+remaining universes are the ones declared. In the term and in general in
+proof mode, introduced universe names can be referred to in
+terms. Note that local universe names shadow global universe names.
+During a proof, one can use \texttt{Show Universes} to display
+the current context of universes.
 
 Definitions can also be instantiated explicitly, giving their full instance:
 \begin{coq_example}
 Check (pidentity@{Set}).
-Check (le@{i j}).
+Universes k l.
+Check (le@{k l}).
 \end{coq_example}
 
 User-named universes are considered rigid for unification and are never
 minimized.
 
-Finally, two commands allow to name \emph{global} universes and constraints.
-
-\subsection{\tt Universe {\ident}.
-  \comindex{Universe}
-  \label{UniverseCmd}}
+\subsection{\tt Unset Strict Universe Declaration.
+  \optindex{StrictUniverseDeclaration}
+  \label{StrictUniverseDeclaration}}
 
-This command declare a new global universe named {\ident}.
-
-\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}.
-  \comindex{Constraint}
-  \label{ConstraintCmd}}
-
-This command declare a new constraint between named universes. 
-The order relation can be one of $<$, $<=$ or $=$. If consistent, 
-the constraint is then enforced in the global environment.
-
-\begin{ErrMsgs}
-\item \errindex{Undeclared universe {\ident}}.
-\item \errindex{Universe inconsistency}
-\end{ErrMsgs}
+The command \texttt{Unset Strict Universe Declaration} allows one to
+freely use identifiers for universes without declaring them first, with
+the semantics that the first use declares it. In this mode, the universe
+names are not associated with the definition or proof once it has been
+defined. This is meant mainly for debugging purposes.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 064dde3a6..6c2316988 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1768,7 +1768,7 @@ struct
 
   let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+      h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -1842,7 +1842,7 @@ struct
 
   let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+      h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 82c068be0..4a9466f4f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -280,9 +280,8 @@ type evar_universe_context =
    uctx_univ_variables : Universes.universe_opt_subst;
    (** The local universes that are unification variables *)
    uctx_univ_algebraic : Univ.universe_set; 
-   (** The subset of unification variables that
-	can be instantiated with algebraic universes as they appear in types 
-	and universe instances only. *)
+   (** The subset of unification variables that can be instantiated with
+	algebraic universes as they appear in inferred types only. *)
    uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
    uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
  }
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d484df69c..d354a6c3c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -118,7 +118,7 @@ let _ =
 	  { optsync  = true;
             optdepr  = false;
 	    optname  = "minimization to Set";
-	    optkey   = ["Universe";"set";"Minimization"];
+	    optkey   = ["Universe";"Minimization";"ToSet"];
 	    optread  = Universes.is_set_minimization;
 	    optwrite = (:=) Universes.set_minimization })