Doesn't this mean we can revert fad781af?
It probably does, but I wanted to wait until the PR lands in Coq just to be sure.