diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-06 13:36:47 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:30:12 +0100 |
| commit | af5eded304b74fa0fccb35a7dc284c46a96ba5cc (patch) | |
| tree | fff5fc5a1c9cd2196b5f46fa173fc3530fb58996 /CHANGES | |
| parent | 2e30531e78519a5b9c3773c2524e4fd4759cc5c8 (diff) | |
Documentation for Cumulativity Weak Constraints.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 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 |