Cannot require list module any more without importing it

Report on the Rocq forum:

I want to use some theorems from the list module of stdpp. I don’t want to Import it because it is a large library and it clutters the global namespace with notation and names that I want to use for other things (like partition).

...

In previous versions of Rocq/Coq this worked fine, but after upgrading from 8.20.0 to 9.0.0 this no longer works. It seems that the list module re-exports list_basics, list_monad etc., which each internally define their own list module that exports its symbols (see stdpp.list), but this does not work well when using Require only…

Selective import Import list_basics(elem_of_cons). does work, but does not play well with notations like Notation head := hd_error., and it would be rather tedious to do this for every symbol I want to refer to, and the documentation notes that I should not rely on the organization of these internal modules.