open hiding notation

Stream: lean4

[Patrick Massot]

Is there anyway to tell the open command to hide some scoped notation? Someone had the very bad idea of writing @[inherit_doc goldenRatio] scoped[Real] notation "φ" => goldenRatio and open Real is a very common line. The long-term fix is of course to put this notation is a much more specific namespace, but is there a stop gap?

[Patrick Massot]

I opened #7871 for the Mathlib fix.

[Patrick Massot]

I'm fairly confident that CI will like it since I would be very surprised if this file were imported anywhere.

[Damiano Testa]

Mathlib.lean is the only file importing it...

[Eric Wieser]

One option is just to put all of this kind of thing in a Foo.Notation namespace

[Eric Wieser]

I don't really understand why we combined open and open_locale, it's not all that common for their roles to intersect.