Closed herbelin closed 6 months ago
To be considered synchronously with coq/coq#18397.
Upstream PR merged, this can be merged
To be considered synchronously with coq/coq#18397.