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: https://mattermost.mpi-sws.org/iris/pl/xdgqgkyw9ifcmj3zdsy8dyb18e 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

Loading