@@ -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] [#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.
*[MEDIUM] [#9135](https://github.com/coq/coq/issues/9135)`refine` and friends ignore `Opaque`. See https://gitlab.mpi-sws.org/iris/iris/issues/301 for the corresponding issue in Iris.
