Skip to content
Snippets Groups Projects

rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)

Passed
Ralf Jung created pipeline for commit 71bce7f8
, finished
Related merge request !301 to merge ralf/map_union_subseteq
merge request
2 jobs 4 minutes 45 seconds, queued for 9 seconds