Skip to content
GitLab

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

Merged Robbert Krebbers requested 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.