... | ... | @@ -27,15 +27,12 @@ Priority [HIGH] means that this actively affects how we do things and we have no |
|
|
### Miscellaneous
|
|
|
|
|
|
* [HIGH] [#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.
|
|
|
* [MEDIUM] [#13654](https://github.com/coq/coq/issues/13654): `Custom Entry` export behavior is broken. Work-around: no custom entry, a lot of notation duplication.
|
|
|
* [MEDIUM] [#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.
|
|
|
* [MEDIUM] [#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`.)
|
|
|
* [MEDIUM] [#12011](https://github.com/coq/coq/issues/12011): `rewrite ... in` (ssreflect) fails where `rewrite -> ... in` works. Work-around: Use the latter instead of the former.
|
|
|
* [LOW] [#6042](https://github.com/coq/coq/issues/6042): `Generalizable All Variables` affects `Instance`.
|
|
|
* [LOW] [#9661](https://github.com/coq/coq/issues/9661): Cannot disable generalization of implicit arguments in `` `{...} ``.
|
|
|
|
|
|
# Coq Bugs recently fixed / features recently introduced that we are not (yet) taking advantage of
|
|
|
|
|
|
* [#6923](https://github.com/coq/coq/pull/6923): Proper control over how `Set` is propagated on imports. Available since 8.8.
|
|
|
* [#7910](https://github.com/coq/coq/issues/7910): We can control type-checking to be more bidirectional, which helps enormously with telescopes and the like. Available starting with 8.11.
|
|
|
* [#10076](https://github.com/coq/coq/pull/10076): We can make some projections non-canonical, to hopefully fix all these "redundant-canonical-projection" warnings. Available starting with 8.11.
|
|
|
* [#13996](https://github.com/coq/coq/issues/13996): We should be able to implement `string_to_ident` without FFI tricks or `intros_by_string`. Available starting with 8.14. |