rename Z2Nat_inj_div and Z2Nat_inj_mod (!161) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Michael Sammler requested to merge msammler/rename_Nat2Z_inj_div into master 4 years ago

1 unresolved thread

This MR renames Z2Nat_inj_div, Z2Nat_inj_mod, Nat2Z_inj_div and Nat2Z_inj_mod to follow the naming conventions of Z2Nat and Nat2Z. See !136 (comment 49866)

Should I mention iris-users here already or only if the MR is merged?

Activity

Ralf Jung @jung · 4 years ago

Owner

Should I mention iris-users here already or only if the MR is merged?

Let's do it when it gets merged to not bore them with the review discussion.
Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 4 years ago

CHANGELOG.md

 ## std++ master
 - Rename `Z2Nat_inj_div` and `Z2Nat_inj_mod` to `Nat2Z_inj_div` and
   `Nat2Z_inj_mod` to follow the naming convention of `Nat2Z` and
   `Z2Nat`.

Michael Sammler added 1 commit 4 years ago

added 1 commit

0eaae21d - rename Z2Nat_inj_div and Z2Nat_inj_mod

Compare with previous version

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

@iris-users this is a breaking change.

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

merging.

Robbert Krebbers mentioned in commit 4 years ago

mentioned in commit ea934fb9

Robbert Krebbers merged 4 years ago

merged

Please register or sign in to reply