Clarify relationship between `gset_to_gmap` and `set_to_map`.
Passed
Robbert Krebbers
created pipeline for commit
4bea88d1
, finished
Related merge request !371 to merge robbert/gset_to_gmap
4 minutes 16 seconds, queued for 4 seconds