Document anonymous universes (PR #544).

1 files changed, 12 insertions, 2 deletions

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index cd36d1d320..6ea2537399 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -332,8 +332,18 @@ Universes k l.
 Check (le@{k l}).
 \end{coq_example}
 
-User-named universes are considered rigid for unification and are never
-minimized.
+User-named universes and the anonymous universe implicitly attached to
+an explicit $Type$ are considered rigid for unification and are never
+minimized. Flexible anonymous universes can be produced with an
+underscore or by omitting the annotation to a polymorphic definition.
+
+\begin{coq_example}
+  Check (fun x => x) : Type -> Type.
+  Check (fun x => x) : Type -> Type@{_}.
+
+  Check le@{k _}.
+  Check le.
+\end{coq_example}
 
 \subsection{\tt Unset Strict Universe Declaration.
   \optindex{Strict Universe Declaration}