Closed proux01 closed 1 month ago
To be merged in sync with https://github.com/coq/coq/pull/19149
No longer needed, sorry for the noise
To be merged in sync with https://github.com/coq/coq/pull/19149