... | ... | @@ -6,17 +6,21 @@ 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`.
|
|
|
|
|
|
Bugs for which we carry "good enough" work-arounds, or that influenced the design:
|
|
|
|
|
|
* [#7773](https://github.com/coq/coq/issues/7773): `setoid_rewrite` fails where (ssreflect) `rewrite` and `rewrite ->` succeed. Work-around: Don't use `setoid_rewrite`. (So far, no case has come up where we absolutely needed `setoid_rewrite`.)
|
|
|
* [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have the (expected) effect. Work-around: `Class NoBackTrack`.
|
|
|
* [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well. Work-around: *unknown*.
|
|
|
* [#6294](https://github.com/coq/coq/issues/6294): `apply` (including TC search) and canonical structures don't mix very well. Work-around: **unknown**.
|
|
|
* [#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`.
|
|
|
|
|
|
Nuisances affecting us but not changing the way we do things:
|
|
|
|
|
|
* [#6042](https://github.com/coq/coq/issues/6042): `Generalizable All Variables` affects `Instance`.
|
|
|
* [#5699](https://github.com/coq/coq/issues/5699), [#5698](https://github.com/coq/coq/issues/5698), [#5250](https://github.com/coq/coq/issues/5250): Primitive projections behave strange.
|
|
|
* [#5698](https://github.com/coq/coq/issues/5698), [#5250](https://github.com/coq/coq/issues/5250): Primitive projections behave strange.
|
|
|
|
|
|
# Coq Bugs recently fixed that we are not (yet) taking advantage of
|
|
|
|
... | ... | |