... | ... | @@ -38,3 +38,4 @@ Priority [HIGH] means that this actively affects how we do things and we have no |
|
|
* [#6923](https://github.com/coq/coq/pull/6923): Proper control over how `Set` is propagated on imports. Available since 8.8.
|
|
|
* [#7910](https://github.com/coq/coq/issues/7910): We can control type-checking to be more bidirectional, which helps enormously with telescopes and the like. Available starting with 8.11.
|
|
|
* [#10076](https://github.com/coq/coq/pull/10076): We can make some projections non-canonical, to hopefully fix all these "redundant-canonical-projection" warnings. Available starting with 8.11.
|
|
|
* [#13996](https://github.com/coq/coq/issues/13996): We should be able to implement `string_to_ident` without FFI tricks or `intros_by_string`. Available starting with 8.14. |