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.

---
 doc/refman/Universes.tex | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'doc')

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