semi_additive is also defined in MathComp 2

[affeldt-aist]

analysis/theories/measure.v

Line 1296 in b1a0e33

Definition semi_additive := forall F n,

this will conflict with Nmodule @proux01

[proux01]

They remain accessible as GRing.semi_additive and measure.semi_additive so it doesn't look that catastrophic.

[affeldt-aist]

I didn't mean to sound catastrophic ^_^, I just thought that it might be a good timing to think of a name change, I don't think that the semi_ prefix here is as important as it is for NModule @CohenCyril (no hurry anyway)

[affeldt-aist]

NB: not addressed yet but considered low priority, discussed during the following meeting https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting