to_additive documentation bug

Stream: general

[Yaël Dillies]

docs#finset.sum_comp is weirdly declared. Instead of tagging docs#finset.prod_comp, it was additivized by hand and later tagged to_additive. The later tagging adds a docstring, as shown by the source, but it seems to get ignored because it's not visible in the docs.