Closed vbgl closed 4 years ago
This is an overlay for https://github.com/coq/coq/pull/11018
@vbgl this looks all good and backwards-compatible to me, should I merge right now or will you give the word?
This is a trivial change, so you can merge it whenever you want. Thanks.
This is an overlay for https://github.com/coq/coq/pull/11018