... | ... | @@ -15,7 +15,7 @@ Bugs for which we carry "good enough" work-arounds, or that influenced the desig |
|
|
* [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have the (expected) effect. Work-around: `Class NoBackTrack`.
|
|
|
* [#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`.
|
|
|
* **#????**: 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`.
|
|
|
* [#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`.
|
|
|
|
|
|
Nuisances affecting us but not changing the way we do things:
|
|
|
|
... | ... | |