-
Robbert Krebbers authored
Rename `option_mbind_proper` → `option_bind_proper` and `option_mjoin_proper` → `option_join_proper`.
Robbert Krebbers authoredRename `option_mbind_proper` → `option_bind_proper` and `option_mjoin_proper` → `option_join_proper`.
