Skip to content

Clarify relationship between `gset_to_gmap` and `set_to_map`.

Robbert Krebbers requested to merge robbert/gset_to_gmap into master

As a response to a question by @jung at Mattermost: I added some comments.

Aside from the differences pointed out in the added comments, the gset function was there before the generic set function.

Merge request reports