... | ... | @@ -6,7 +6,7 @@ Bugs we cannot work around to a satisfying degree: |
|
|
* [#7769](https://github.com/coq/coq/issues/7769): Ltac backtraces show up in proof mode error messages. Partial work-around: Give names to locally bound functions so at least it does not print Ltac source code. However, Ltac function names are still printed.
|
|
|
* [#7910](https://github.com/coq/coq/issues/7910): Type inference needs lots of help for notations involving telescopes, with bad side-effects on printing that same notation.
|
|
|
* [#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`.
|
|
|
* [#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.
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
|
... | ... | |