Skip to content

Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename...

Robbert Krebbersrequested to merge
robbert/fmap_empty into master

Remove duplicate map_fmap_empty of fmap_empty, and rename map_fmap_empty_inv into fmap_empty_inv for consistency's sake.

Merge request reports