FYI these are a few of the many changes in 8.13 w.r.t. notations:
Changed: Redeclaring a notation also reactivates its printing rule; in particular a second Import of the same module reactivates the printing rules declared in this module. In theory, this leads to changes in behavior for printing. However, this is mitigated in general by the adoption in #12986 of a priority given to notations which match a larger part of the term to print (#12984, fixes #7443 and #10824, by Hugo Herbelin).
Changed: Use of notations for printing now gives preference to notations which match a larger part of the term to abbreviate (#12986, by Hugo Herbelin).
Changed: Scope information is propagated in indirect applications to a reference prefixed with @; this covers for instance the case r.(@p) t where scope information from p is now taken into account for interpreting t (#12685, by Hugo Herbelin).