| ... | ... | @@ -29,10 +29,10 @@ Priority [HIGH] means that this actively affects how we do things and we have no |
|
|
|
* [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`.)
|
|
|
|
* [LOW] [#9661](https://github.com/coq/coq/issues/9661): Cannot disable generalization of implicit arguments in `` `{...} ``.
|
|
|
|
* [MEDIUM] [#16042](https://github.com/coq/coq/issues/16042): Cannot use `binder` for WP notations as that causes parsing conflicts.
|
|
|
|
|
|
|
|
# Coq Bugs recently fixed / features recently introduced that we are not (yet) taking advantage of
|
|
|
|
|
|
|
|
* [#13265](https://github.com/coq/coq/pull/13265) (8.13): using `v closed binder` for `WP` notation (and other use-cases like big-ops). Unfortunately blocked by [#16042](https://github.com/coq/coq/issues/16042).
|
|
|
|
* [#13996](https://github.com/coq/coq/issues/13996) (8.14): We should be able to implement `string_to_ident` without FFI tricks or `intros_by_string`.
|
|
|
|
* [#14548](https://github.com/coq/coq/issues/14548) (8.15): Name mangling "light"
|
|
|
|
* [#13969](https://github.com/coq/coq/pull/13969) (soon to be on master): lets us use mode `! !` for `Reflexive`
|
| ... | ... | |
