Coq PR #12950, among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing
le n m as either
m <= n or
m ≤ n, due to the order of imports between
The Coq PR is still at the beginning of a process of discussion but the change to stdpp is backward compatible (as far as I can judge) and it should be safe to merge it anyway.