@@ -23,6 +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.
