Closed proux01 closed 2 years ago
To be merged in sync with the upstream PR https://github.com/coq/coq/pull/15884
Please merge, now that upstream PR https://github.com/coq/coq/pull/15884 is merged.
To be merged in sync with the upstream PR https://github.com/coq/coq/pull/15884