Remove FIXME in `fin_map_dom`.
Passed
Robbert Krebbers
created pipeline for commit
b0eea606
, finished
Related merge request !483 to merge robbert/remove_fixme
6 minutes 7 seconds, queued for 3 seconds