Skip to content
Snippets Groups Projects
Commit 5710f90e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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

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

This was pointed out by @atrieu in !175 (comment 53746)
parent ef460edd
No related branches found
No related tags found
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment