@@ -25,6 +25,7 @@ Priority [HIGH] means that this actively affects how we do things and we have no
...
@@ -25,6 +25,7 @@ Priority [HIGH] means that this actively affects how we do things and we have no
### Miscellaneous
### 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.
*[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.
*[HIGH] [#15768](https://github.com/coq/coq/issues/15768): it is not possible to stop `simpl` from unfolding some functions in some situations.
*[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] [#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] [#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] [#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`.)
