Union precedence

Stream: general

[Patrick Massot]

I don't remember whether there is a reason why we are still stuck with precedences that force writing: (⋃ j, s j) = univ instead of ⋃ j, s j = univ. I thought this was fixed. Or maybe we fixed supr and infi but not union and intersection? Does someone remember?

[Eric Wieser]

I think we were waiting for the notation to move out of core (which it only just did)