Make sum_inhabited_r not a copy of sum_inhabited_l

This existed at least as far back as 361308c7, 8 years ago.

added 15 commits

• 5c44d8d8...fe3b9967 - 14 commits from branch iris:master
• cedb9df5 - Make sum_inhabited_r not a copy of sum_inhabited_l

Compare with previous version

Thanks for the fix.

And thanks for looking up the history, that was one massive commit back then...

merged

mentioned in commit 69e109d6

Whoops, sorry, wasn't done rebuilding stdpp and iris! Thanks for the fast merge and hope nothing breaks!

This should get a changelog entry.

It seems like a trivial bug fix to me, unless anyone relies on Inhabited (A + B) failing, this should have no impact.

That said, if you want to have a CHANGELOG entry, go for it.

It seems like a trivial bug fix to me,

Correct. And bugfixes should get a changelog. :)

If we go that way, then everything should have a CHANGELOG, including for example !285 (diffs)

Those are not bugfixes; we are less consistent with changelogs for new things.

/me starts thinking of a better changelog... Oh, thanks for adding it Ralf :-)