diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | doc/refman/Universes.tex | 14 |
2 files changed, 18 insertions, 0 deletions
@@ -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 |