Closed herbelin closed 3 weeks ago
To be merged synchronously with coq/coq#19075. Thanks in advance.
Please merge now.
Will merge as soon as CI passes.
To be merged synchronously with coq/coq#19075. Thanks in advance.