See https://github.com/coq/coq/pull/16748#issuecomment-1296962224
merged
mentioned in commit c59b6199
mentioned in merge request !479 (merged)