... | ... | @@ -4,7 +4,6 @@ Priority [HIGH] means that this actively affects how we do things and we have no |
|
|
|
|
|
### Typeclasses
|
|
|
|
|
|
- [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`.
|
... | ... | @@ -35,3 +34,4 @@ Priority [HIGH] means that this actively affects how we do things and we have no |
|
|
|
|
|
* [#7910](https://github.com/coq/coq/issues/7910): We can control type-checking to be more bidirectional, which helps enormously with telescopes and the like. Available starting with 8.11.
|
|
|
* [#13996](https://github.com/coq/coq/issues/13996): We should be able to implement `string_to_ident` without FFI tricks or `intros_by_string`. Available starting with 8.14.
|
|
|
* [#9058](https://github.com/coq/coq/issues/9058): We should experiment with `Hint Mode Equiv ! : typeclass_instances`. Available starting with 8.12. |
|
|
\ No newline at end of file |