Closed maximedenes closed 1 year ago
This is necessary for https://github.com/coq/coq/pull/16578, but should be backward compatible.
This is necessary for https://github.com/coq/coq/pull/16578, but should be backward compatible.