Expand Credits for 8.5 and doc on universes

3 files changed, 58 insertions, 16 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index f683e4543b..35d64053c1 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -10,7 +10,7 @@
 \label{typeclasses}
 
 \begin{flushleft}
-  \em The status of Type Classes is (extremely) experimental.
+  \em The status of Type Classes is experimental.
 \end{flushleft}
 
 This chapter presents a quick reference of the commands related to type
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index ef7a61931c..46ee361e09 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -980,16 +980,28 @@ help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
 Faithfull and Jesper Bengtson).  The development of such features was
 funded by the Paral-ITP French ANR project.
 
-The universe polymorphism extension is based on a change of the kernel
-architecture to handle constraint checking only, leaving the generation
-of constraints outside it.
+The full universe polymorphism extension was designed by Matthieu
+Sozeau. It conservatively extends the universes system and core calculus
+with definitions and inductive declarations parameterized by universes
+and constraints. It is based on a change of the kernel architecture to
+handle constraint checking only, leaving the generation of constraints
+to the refinement/type inference engine. Accordingly, tactics are now
+fully universe aware, resulting in more localized error messages in case
+of inconsistencies and allowing higher-level algorithms like unification
+to be entirely type safe. The internal representation of universes has
+been modified but this invisible to the user. 
 
 The underlying logic has been extended with $\eta$-conversion for
-primitive records thanks to Matthieu Sozeau. This additional form of
-$\eta$-conversion is justified using the same principle than the
-previously added $\eta$-conversion for function types, based on
-formulations of the Calculus of Inductive Constructions with typed
-equality.
+records defined with primitive projections by Matthieu Sozeau. This
+additional form of $\eta$-conversion is justified using the same
+principle than the previously added $\eta$-conversion for function
+types, based on formulations of the Calculus of Inductive Constructions
+with typed equality. Primitive projections, which do not carry the
+parameters of the record and are rigid names (not defined as a
+pattern-matching construct), make working with nested records more
+manageable in terms of time and space consumption. This extension and
+universe polymorphism were carried partly while the author was working
+at the IAS in Princeton.
 
 The guard condition has been made compliant with extensional equality
 principles such as propositional equality and univalence, thanks to
@@ -1021,7 +1033,7 @@ Pierre Courtieu contributed new features for using {\Coq} through Proof
 General and for better interactive experience (bullets, Search etc).
 
 \begin{flushright}
-Paris, Janvier 2015\\
+Paris, January 2015\\
 Hugo Herbelin \& Matthieu Sozeau\\
 \end{flushright}
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 530086961f..4b71a25867 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -6,6 +6,12 @@
 
 \asection{General Presentation}
 
+\begin{flushleft}
+  \em The status of Universe Polymorphism is experimental. Some features
+  are not compatible with it (yet): native compilation and bytecode
+  compilation do not handle polymorphic definitions.
+\end{flushleft}
+
 This section describes the universe polymorphic extension of Coq.
 Universe polymorphism allows writing generic definitions making use of
 universes and reuse them at different and sometimes incompatible levels.
@@ -119,7 +125,7 @@ producing global universe constraints, one can use the
   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 introduce global universes, making the two definitions depend on
+  which introduces global universes, making the two definitions depend on
   the \emph{same} universes associated to the variable.
 \item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint
   polymorphically, not at a single instance.
@@ -133,17 +139,41 @@ references. The semantics respect the fact that definitions are
 transparent, so indistinguishable from their bodies during conversion.
 
 This is accomplished by changing one rule of unification, the
-first-order approximation rule:
-
+first-order approximation rule, which applies when two applicative terms
+with the same head are compared. It tries to short-cut unfolding by
+comparing the arguments directly. In case the constant is universe
+polymorphic, we allow this rule to fire only when unifying the universes
+results in instantiating a so-called flexible universe variables (not
+given by the user). Similarly for conversion, if such an equation of
+applicative terms fail due to a universe comparison not being satisfied,
+the terms are unfolded. This change implies that conversion and
+unification can have different unfolding behaviors on the same
+development with universe polymorphism switched on or off.
 
-TODO
+\asection{Explicit Universes}
 
+\begin{flushleft}
+  \em The design and implementation of explicit universes is very
+  experimental and is likely to change in future versions.
+\end{flushleft}
 
+The syntax has been extended to allow users to explicitely bind names to
+universes and explicitely instantantiate polymorphic
+definitions. Currently, binding is implicit at the first occurrence of a 
+universe name. For example below, i and j are introduced by the
+annotations attached to Types. 
 
-\asection{Explicit Universes}
+\begin{coq_example*}
+Polymorphic Definition le (A : Type@{i}) : Type@{j} := A.
+\end{coq_example*}
 
-TODO
+Definitions can also be instantiated explicitely:
+\begin{coq_example}
+Check (pidentity@{Set}).
+Check (le@{Type Set}).
+\end{coq_example}
 
+User-named universes are considered rigid for unification.
 
 %%% Local Variables: 
 %%% mode: latex