This is backward compatible so can be merged before the parent PR https://github.com/coq/coq/pull/16788
