... | ... | @@ -11,7 +11,7 @@ There [is a prototype plugin](https://github.com/ppedrot/coq-string-ident), but |
|
|
### Typeclasses
|
|
|
|
|
|
- [HIGH] [#5752](https://github.com/coq/coq/issues/5752): `Hint Mode` behaves differently for local context
|
|
|
- [HIGH] [#5735](https://github.com/coq/coq/issues/5735): `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] [#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`.
|
|
|
- [MEDIUM] [#7914](https://github.com/coq/coq/issues/7914): TC resolution is unable to use the fact that `Prop` is a subtype of `Type`. Work-around: Have a separate typeclass `IntoPureT` that uses `refine` through a `Hint Extern`.
|
... | ... | |