... | ... | @@ -23,7 +23,6 @@ There [is a prototype plugin](https://github.com/ppedrot/coq-string-ident), but |
|
|
### Unification / Type inference
|
|
|
|
|
|
* [HIGH] [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well, so we randomly use `apply:` and cannot grow our algebraic hierarchy any further.
|
|
|
* [HIGH] [#7910](https://github.com/coq/coq/issues/7910): Type inference needs lots of help for notations involving telescopes, with bad side-effects on printing that same notation. We have to write tons of annotations in our notation and live with printing not always working. (We could duplicate our notations to work around that but that's be lots of code duplication.)
|
|
|
|
|
|
### Primitive projections
|
|
|
|
... | ... | @@ -40,4 +39,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. |
|
|
\ No newline at end of file |
|
|
* [#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. |
|
|
\ No newline at end of file |