... | ... | @@ -15,7 +15,7 @@ Bugs for which we carry "good enough" work-arounds, or that influenced the desig |
|
|
|
|
|
* [#2901](https://github.com/coq/coq/issues/2901): `destruct H` does not clear `H` if it is a section variable. Work-around in `naive_solver`: Clear manually.
|
|
|
* [#5699](https://github.com/coq/coq/issues/5699): `rewrite /foo` does not work for primitive projections. Work-around: Use `unfold`.
|
|
|
* [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have the (expected) effect. Work-around: `Class NoBackTrack`.
|
|
|
* [#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`.
|
|
|
* [#7773](https://github.com/coq/coq/issues/7773): `setoid_rewrite` fails where (ssreflect) `rewrite` and `rewrite ->` succeed. Work-around: Don't use `setoid_rewrite`. (So far, no case has come up where we absolutely needed `setoid_rewrite`.)
|
|
|
* [#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`.
|
|
|
|
... | ... | |