search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
197 stars 44 forks source link

`semi_additive` is also defined in MathComp 2 #1072

Open affeldt-aist opened 10 months ago

affeldt-aist commented 10 months ago

https://github.com/math-comp/analysis/blob/b1a0e33f32bb2f865372d0963afb22b5ad9eadf3/theories/measure.v#L1296

this will conflict with Nmodule @proux01

proux01 commented 10 months ago

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

affeldt-aist commented 10 months ago

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 `semiprefix here is as important as it is forNModule` @CohenCyril (no hurry anyway)