... | ... | @@ -8,6 +8,7 @@ Bugs we cannot work around to a satisfying degree: |
|
|
* [#4381](https://github.com/coq/coq/issues/4381): `Tactic Notation` cannot set a scope for `constr` arguments, so we very often have to write `%I` manually.
|
|
|
* [#6583](https://github.com/coq/coq/issues/6583): `apply` triggers TC resolution on unrelated goals. Work-around: Use `typeclasses eauto` instead of `apply _` and otherwise `notypeclasses refine` instead of `apply`. It's hard to tell if we got this all right, though, and it may not just be `apply` that does this.
|
|
|
* [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well.
|
|
|
* [#7916](https://github.com/coq/coq/issues/7916): Cannot set mode for `Reflexive` because `setoid_rewrite` makes some strange queries.
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
|
... | ... | |