CHANGELOG.md · ee76981dfcf45bcf56c02d0b5d98023d93f6b7f4 · Iris / stdpp · GitLab

Snippets Groups Projects

4 years ago

Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`, · 5710f90e

Robbert Krebbers authored 4 years ago

and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.

This was pointed out by @atrieu in !175 (comment 53746)

5710f90e

Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`,

Robbert Krebbers authored 4 years ago

and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.

This was pointed out by @atrieu in !175 (comment 53746)

To find the state of this project's repository at the time of any of these versions, check out the tags.