... | ... | @@ -3,12 +3,13 @@ |
|
|
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.
|
|
|
* [#5735](https://github.com/coq/coq/issues/5735): Cannot use `Hint Mode Equiv ! : typeclass_instances`.
|
|
|
* [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well.
|
|
|
* [#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.
|
|
|
* [#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.
|
|
|
* [#7916](https://github.com/coq/coq/issues/7916): Cannot set mode for `Reflexive` because `setoid_rewrite` makes some strange queries.
|
|
|
* [#5735](https://github.com/coq/coq/issues/5735): Cannot use `Hint Mode Equiv ! : typeclass_instances`, so we suffer from backtracking and loops whenever `Equiv ?` comes up.
|
|
|
* [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well, so we randomly use `apply:` and cannot grow our algebraic hierarchy any further.
|
|
|
* [#6583](https://github.com/coq/coq/issues/6583): `apply` triggers TC resolution on unrelated goals so proof mode tactics randomly fail when the user has other typeclass goals open. 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.
|
|
|
* [#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.
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
|
... | ... | |