... | ... | @@ -4,7 +4,6 @@ Priority [HIGH] means that this actively affects how we do things and we have no |
|
|
|
|
|
### Typeclasses
|
|
|
|
|
|
- [HIGH] [#5752](https://github.com/coq/coq/issues/5752): `Hint Mode` behaves differently for local context
|
|
|
- [HIGH] [#9058](https://github.com/coq/coq/issues/9058): `Hint Mode` cancels entire search too early. For this reason we cannot use `Hint Mode Equiv ! : typeclass_instances`, so we suffer from backtracking and loops whenever `Equiv ?` comes up.
|
|
|
- [HIGH] [#7916](https://github.com/coq/coq/issues/7916): Cannot set mode for `Reflexive` because `setoid_rewrite` makes some strange queries, so we suffer from backtracking and slow rewriting whenever `Reflexive ?` comes up.
|
|
|
- [MEDIUM] [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have any (or at least not the expected) effect. Work-around: `Class NoBackTrack`.
|
... | ... | |