Rename `option_union_Some` → `union_Some`

See discussion at !432 (comment 87085)

This removes option_ if there's already something else in the name to disambiguate, here that is _Some.

We could also prefix everything with option_, but that would require more changes. For better or worse, I think this MR matches the consensus we also have for lists, maps, sets (e.g., having lookup_app_Some instead of list_lookup_app_Some).

added S-waiting-for-review label

added 66 commits

• 79cc350a...137be24a - 64 commits from branch master
• 0fbe067f - Rename `option_union_Some` → `union_Some`.
• 67f14fc4 - CHANGELOG.

Compare with previous version

added 1 commit

• 7ff6b913 - CHANGELOG.

Compare with previous version

enabled an automatic merge when the pipeline for 7ff6b913 succeeds

@iris-users

• Rename option_union_Some → union_Some.

removed S-waiting-for-review label

merged

mentioned in commit 20813c6c