Skip to content

Rename `option_union_Some` → `union_Some`

Robbert Krebbersrequested to merge
robbert/union_Some into master

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).

Merge request reports