Adapt to https://github.com/coq/coq/pull/19530
This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the future).
Merging this is not required for the upstream PR, you can do whatever you want with it.
Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the future). Merging this is not required for the upstream PR, you can do whatever you want with it.