I am getting a lot of warnings like these:
[notation-overridden,parsing]
Warning: Notation _ ≠ _ was already used in scope type_scope.
[notation-overridden,parsing]
If there is a way to avoid these, short of totally disabling notation overriding warnings globally?