Skip to content
GitLab

Rename instance `finmap_lookup_total` → `map_lookup_total`.

Merged Robbert Krebbers requested to merge robbert/map_lookup_total into master

This this is an instance, not a definition, it should not affect anyone.

Merge request reports