Skip to content

Conversation

@affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Mar 14, 2023

Motivation for this change

This addresses the first part of issue #860 and can already be merged since is is moreover used in PR #873
(that is just a renaming that anticipates in particular the fact that the operator of convex spaces in PR #873 is naturally called conv)

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist added this to the 0.6.2 milestone Mar 14, 2023
@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Mar 15, 2023
@affeldt-aist
Copy link
Member Author

Since this renaming was part of a discussion with @CohenCyril @ybertot @t6s I guess we can merge in the interest of time (it is used in PR #873 ).

@affeldt-aist affeldt-aist requested a review from t6s March 20, 2023 09:41
@CohenCyril CohenCyril added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Mar 27, 2023
@affeldt-aist
Copy link
Member Author

It was brought to my attention that line_path might be a bit long after all.
I am not sure but anyway since PR #873 is underway we will have the occasion pretty soon to discuss the naming again if necessary.

@affeldt-aist affeldt-aist requested review from t6s and removed request for t6s April 7, 2023 05:22
@affeldt-aist affeldt-aist mentioned this pull request Apr 10, 2023
@affeldt-aist affeldt-aist requested review from proux01 and removed request for t6s April 12, 2023 09:12
@proux01 proux01 merged commit 0474048 into math-comp:master Apr 12, 2023
@affeldt-aist affeldt-aist deleted the set_interval_20230314 branch April 12, 2023 09:22
@proux01 proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Apr 13, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

renaming/refactoring 🔧 This is about a renaming or refactoring in the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants