Get rid of a superflous argument to `fresh_locs`. (!288) · Merge requests · Iris / Iris · GitLab

Snippets Groups Projects

Merged Dan Frumin requested to merge dfrumin/iris-coq:fresh_locs_arg into master 5 years ago

The argument is not really used (at least right now).

Activity

Robbert Krebbers @robbertkrebbers · 5 years ago

Owner

I think I proposed this in order to have a very generic API. However, even if we would switch to the CompCert memory model, this argument is not needed. So I would be in favor of merging this, since it causes more confusion than it's potentially useful.

Edited 5 years ago by Robbert Krebbers
Ralf Jung @jung · 5 years ago

Owner

I don't really care.
Robbert Krebbers mentioned in commit 64c16f99 5 years ago

mentioned in commit 64c16f99
Robbert Krebbers merged 5 years ago

merged
Robbert Krebbers @robbertkrebbers · 5 years ago

Owner

That was easy! Merging then :)
Robbert Krebbers @robbertkrebbers · 5 years ago

Owner

And thanks @dfrumin!
Robbert Krebbers mentioned in commit transfinite@e1198994 4 years ago

mentioned in commit transfinite@e1198994

Please register or sign in to reply