... | ... | @@ -9,7 +9,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 so the user is presented with (sometimes huge) amounts of noise. 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. We have to write tons of annotations in our notation and live with printing not always working. (We could duplicate our notations to work around that but that's be lots of code duplication.)
|
|
|
* [#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.
|
|
|
* **#????**: Cannot convert between strings and identifiers in Ltac, leading to horrible code and lots of hacks all over the place.
|
|
|
* [#7922](https://github.com/coq/coq/issues/7922): Cannot convert between strings and identifiers in Ltac, leading to horrible code and lots of hacks all over the place.
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
|
... | ... | |