diff options
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -95,6 +95,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 |