... | ... | @@ -23,7 +23,7 @@ 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.
|
|
|
* [MEDIUM] `refine` and friends ignore type class opacity. See https://gitlab.mpi-sws.org/iris/iris/issues/301#note_46408.
|
|
|
* [MEDIUM] [#9135](https://github.com/coq/coq/issues/9135) `refine` and friends ignore `Opaque`. See https://gitlab.mpi-sws.org/iris/iris/issues/301#note_46408.
|
|
|
|
|
|
### Primitive projections
|
|
|
|
... | ... | |