From 45a18537a5aba4bb9b4be957a3818d1e004d4246 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 16 Aug 2017 22:11:40 +0200
Subject: Document anonymous universes (PR #544).

---
 doc/refman/Universes.tex | 14 ++++++++++++--
 1 file 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}
-- 
cgit v1.2.3