From af5eded304b74fa0fccb35a7dc284c46a96ba5cc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Mar 2018 13:36:47 +0100
Subject: Documentation for Cumulativity Weak Constraints.

---
 CHANGES                  |  4 ++++
 doc/refman/Universes.tex | 14 ++++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/CHANGES b/CHANGES
index a514f5934c..ef94fde567 100644
--- a/CHANGES
+++ b/CHANGES
@@ -91,6 +91,10 @@ Universes
 - Universe cumulativity for inductive types is now specified as a
   variance for each polymorphic universe. See the reference manual for
   more information.
+- Inference of universe constraints with cumulative inductive types
+  produces more general constraints. Unsetting new option Cumulativity
+  Weak Constraints produces even more general constraints (but may
+  produce too many universes to be practical).
 - Fix #5726: Notations that start with `Type` now support universe instances
   with `@{u}`.
 - `with Definition` now understands universe declarations
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 6c84a1818c..c7d39c0f3e 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -232,6 +232,20 @@ Section down.
   Defined.
 \end{coq_example}
 
+\subsection{\tt Cumulativity Weak Constraints}
+\optindex{Cumulativity Weak Constraints}
+
+This option, on by default, causes ``weak'' constraints to be produced
+when comparing universes in an irrelevant position. Processing weak
+constraints is delayed until minimization time. A weak constraint
+between {\tt u} and {\tt v} when neither is smaller than the other and
+one is flexible causes them to be unified. Otherwise the constraint is
+silently discarded.
+
+This heuristic is experimental and may change in future versions.
+Disabling weak constraints is more predictable but may produce
+arbitrary numbers of universes.
+
 \asection{Global and local universes}
 
 Each universe is declared in a global or local environment before it can
-- 
cgit v1.2.3