See https://github.com/coq/coq/issues/10480 and https://github.com/coq/coq/issues/10474.
This should be compatible with Coq's master, but I haven't tested.
