Skip to content

Rename `map_preimage` into `map_preimg` (to be consistent with `dom`).

Robbert Krebbers requested to merge robbert/map_preimg into master

For the domain of a map we use dom, not domain.

So it makes sense to also use img instead of image. In !444 (merged) we already do that for the proper image, so let's do too for the pre-image.

Merge request reports

Loading