Nearly additive or multiplicative ?

[fblanqui]

Hi. In realax.ml, line 248, are introduced "nearly additive" functions but, on line 928, they are called "nearly-multiplicative".

[jrh13]

This terminological inconsistency is certainly confusing. It was actually a little result in my PhD thesis that the two things are equivalent (a chapter discusses this reals construction). I'll tweak the comments to make this less confusing.

[aqjune]

It seems the comment has been addressed recently. :)

[jrh13]

Yes indeed, now closed