Stop mentioning Coq bug fixed in Coq >= 8.13

This should wait till stdpp drops support for Coq 8.12, but that's soon.

README.md

@@ -26,10 +26,12 @@ Importing std++ has some side effects as the library sets some global options.
 Notably:
 
 * `Generalizable All Variables`: This option enables implicit generalization in
-  arguments of the form `` `{...}`` (i.e., anonymous arguments).  Unfortunately, it
-  also enables implicit generalization in `Instance`.  We think that the fact
-  that both behaviors are coupled together is a
-  [bug in Coq](https://github.com/coq/coq/issues/6030).
+  arguments of the form `` `{...}`` (i.e., anonymous arguments) and in terms of
+  shape `` `{}``/`` `[]``/`` `()``:
+  https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization
+
+  This also affected `Instance` until Coq 8.12, but since 8.13 it has no other
+  effects (https://github.com/coq/coq/issues/6042).
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.