This is in preparation for coq/coq#9274.
Should be backward compatible but that remains to be tested.
