Merge PR #6775: Allow using cumulativity without forcing strict constraints.

1 files changed, 14 insertions, 0 deletions

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