Fix naming inconsistencies between imset and map lemmas.
#592
Conversation
imset and map lemmas.
|
@CohenCyril @gares can I get an assignee? |
|
@ggonthier @thery could you review this PR? |
CHANGELOG_UNRELEASED.md
Outdated
| @@ -40,6 +40,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). | |||
| - in `finset.v`, new lemmas: `properC`, `properCr`, `properCl` | |||
| - in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl` | |||
| - in `ssrnat.v`, new lemma: `oddS` | |||
| - in `finset.v`, new lemmas: `mem_imset_eq`, `mem_imset2_eq`. | |||
| Ideal names would be `mem_imset` and `mem_imset2`, but these names have just been deprecated from their previous meaning. | |||
There was a problem hiding this comment.
Don't like this idea of temporary name. @maximedenes how coq deals with this kind of situation?
There was a problem hiding this comment.
This strategy was discussed here I cannot recall whether @maximedenes attended though...
There was a problem hiding this comment.
I wasn't there either 😉 still not a fan of temporary names
There was a problem hiding this comment.
You can say "these names will lose the _eq suffix in the next release", it may be of interest to the user. The reason why is not really helping IMO, and here you are not anyway suggesting we plan to use the ideal names in the future.
There was a problem hiding this comment.
I don't recall a case like this in Coq.
There was a problem hiding this comment.
If everybody like temporary names, then @CohenCyril could already make the next pull request for 1.13 so we are sure theses names wil disappear.
There was a problem hiding this comment.
Don't like this idea of temporary name. @maximedenes how coq deals with this kind of situation?
I don't like the temporary names either, but I don't see another way without causing a breaking change. And this seems to minor an issue to cause a breaking change.
You can say "these names will lose the _eq suffix in the next release", it may be of interest to the user. The reason why is not really helping IMO, and here you are not anyway suggesting we plan to use the ideal names in the future.
I was merely following the formulations used by Cyril in #492
If everybody like temporary names, then @CohenCyril could already make the next pull request for 1.13 so we are sure theses names wil disappear.
This is an "after merge" Item, again as in #492
There was a problem hiding this comment.
It can't be a pull request yet, because the things to be removed aren't there yet ...
There was a problem hiding this comment.
@chdoc sorry I am reviewing too many pull requests by cyril I thought it was one of his too.
There was a problem hiding this comment.
It can't be a pull request yet, because the things to be removed aren't there yet ...
Actually, it could be, I did not think about it before, but it just needs to be a pr on top of this one 😆
|
Reworded and rebased. |
|
@thery waiting for your "green tick" ✔️ 😉 |
|
✔️ |
|
... I meant "Approve PR" and stuff, but that works for me too. |
Motivation for this change
fixes #508 (the first stage)
Things done/to do
CHANGELOG_UNRELEASED.md(do not edit former entries)added corresponding documentation in the headersmem_imsert_eqlemmas.Automatic note to reviewers
Read this Checklist and make sure there is a milestone.