Changes

Robbert Krebbers · 4daba54f
--- a/coq-bugs.md
+++ b/coq-bugs.md
-# Coq Bugs affecting Iris development
-
-Priority [HIGH] means that this actively affects how we do things and we have not found a workaround. For [MEDIUM] we have an acceptable workaround or accounted for it sufficiently by changing our design.  The rest is [LOW].
-
-### Typeclasses
-
-  - [HIGH] [#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.
-  - [MEDIUM] [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have any (or at least not the expected) effect. Work-around: `Class NoBackTrack`.
-  - [MEDIUM] [#7914](https://github.com/coq/coq/issues/7914): 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`.
-  - [MEDIUM] [#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.
-  - [LOW] [#7364](https://github.com/coq/coq/issues/7364): Debugging TC issues is very hard.
-  - [LOW] [#9643](https://github.com/coq/coq/issues/9643): We could use better profiling.
-  - [LOW] [#9131](https://github.com/coq/coq/issues/9131): Custom error messages for TC search failure would help for IPM user experience
-
-### Unification / Type inference
-
-* [HIGH] [#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.
-* [MEDIUM] [#9135](https://github.com/coq/coq/issues/9135) `refine` and friends ignore `Opaque`. See https://gitlab.mpi-sws.org/iris/iris/issues/301 for the corresponding issue in Iris.
-
-### Primitive projections
-
-* [MEDIUM] [#5699](https://github.com/coq/coq/issues/5699): `rewrite /foo` does not work for primitive projections. Work-around: Use `unfold`.
-* [LOW] [#5698](https://github.com/coq/coq/issues/5698), [#5250](https://github.com/coq/coq/issues/5250), [#6994](https://github.com/coq/coq/issues/6994): Primitive projections behave strange.
-
-### 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] [#15768](https://github.com/coq/coq/issues/15768): it is not possible to stop `simpl` from unfolding some functions in some situations.
-* [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
-
-* 8.16: [#13969](https://github.com/coq/coq/pull/13969) lets us hopefully use mode `! !` for `Reflexive`
-* 8.16: [reversible coercions](https://mattermost.mpi-sws.org/iris/pl/yz8o9mc7apfupy7h7e3h17kqxc), see [draft MR](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/972)
-* 8.17: [future coercion syntax](https://github.com/coq/coq/pull/16230)
-* 8.19: [`resolve_tc`](https://github.com/coq/coq/pull/13071)
\ No newline at end of file
+# Coq Bugs affecting Iris development
+
+Priority [HIGH] means that this actively affects how we do things and we have not found a workaround. For [MEDIUM] we have an acceptable workaround or accounted for it sufficiently by changing our design.  The rest is [LOW].
+
+### Typeclasses
+
+  - [HIGH] [#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.
+  - [MEDIUM] [#6714](https://github.com/coq/coq/issues/6714): `Set Typeclasses Unique Instances` does not have any (or at least not the expected) effect. Work-around: `Class NoBackTrack`.
+  - [MEDIUM] [#7914](https://github.com/coq/coq/issues/7914): 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`.
+  - [MEDIUM] [#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.
+  - [LOW] [#7364](https://github.com/coq/coq/issues/7364): Debugging TC issues is very hard.
+  - [LOW] [#9643](https://github.com/coq/coq/issues/9643): We could use better profiling.
+  - [LOW] [#9131](https://github.com/coq/coq/issues/9131): Custom error messages for TC search failure would help for IPM user experience
+
+### Unification / Type inference
+
+* [HIGH] [#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.
+* [MEDIUM] [#9135](https://github.com/coq/coq/issues/9135) `refine` and friends ignore `Opaque`. See https://gitlab.mpi-sws.org/iris/iris/issues/301 for the corresponding issue in Iris.
+
+### Primitive projections
+
+* [MEDIUM] [#5699](https://github.com/coq/coq/issues/5699): `rewrite /foo` does not work for primitive projections. Work-around: Use `unfold`.
+* [LOW] [#5698](https://github.com/coq/coq/issues/5698), [#5250](https://github.com/coq/coq/issues/5250), [#6994](https://github.com/coq/coq/issues/6994): Primitive projections behave strange.
+
+### 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] [#15768](https://github.com/coq/coq/issues/15768): it is not possible to stop `simpl` from unfolding some functions in some situations.
+* [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
+
+* 8.16: [#13969](https://github.com/coq/coq/pull/13969) lets us hopefully use mode `! !` for `Reflexive`
+* 8.16: [reversible coercions](https://mattermost.mpi-sws.org/iris/pl/yz8o9mc7apfupy7h7e3h17kqxc), see [draft MR](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/972)
+* 8.17: [future coercion syntax](https://github.com/coq/coq/pull/16230)
+* 8.19: [`resolve_tc`](https://github.com/coq/coq/pull/13071)
+* 8.20: [Smarter guard condition](https://github.com/coq/coq/pull/17986) should allow us to define `fmap`/`mbind` instances for `list` that can be used in nested recursion and do not require the `csimpl` hack.
\ No newline at end of file