Skip to content
Snippets Groups Projects

Clarify relationship between `gset_to_gmap` and `set_to_map`.

Merged 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
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading