... | ... | @@ -42,5 +42,5 @@ There [is a prototype plugin](https://github.com/ppedrot/coq-string-ident), but |
|
|
# Coq Bugs recently fixed / features recently introduced that we are not (yet) taking advantage of
|
|
|
|
|
|
* [#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. Likely available starting with 8.10.
|
|
|
* [#10076](https://github.com/coq/coq/pull/10076): We can make some projections non-canonical, to hopefully fix all these "redundant-canonical-projection" warnings. Likely available starting with 8.10. |
|
|
\ No newline at end of file |
|
|
* [#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. |