|
|
# Coq Bugs affecting Iris development
|
|
|
|
|
|
Bugs we cannot wrok around to a satisfying degree:
|
|
|
|
|
|
* [#5735](https://github.com/coq/coq/issues/5735): Cannot use `Hint Mode Equiv ! : typeclass_instances`.
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
|
|
|
* [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have the (expected) effect. Work-around: `Class NoBackTrack`.
|
|
|
* [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well. Work-around: unknown.
|
|
|
|
|
|
Nuisances affecting us but not changing the way we do things:
|
|
|
|
|
|
* [#6042](https://github.com/coq/coq/issues/6042): `Generalizable All Variables` affects `Instance`. |
|
|
\ No newline at end of file |