Skip to content

mv edist out of urysohn.v - #2119

Merged
affeldt-aist merged 3 commits into
math-comp:masterfrom
affeldt-aist:edist_20261006
Oct 9, 2026
Merged

affeldt-aist merged 3 commits into
math-comp:masterfrom
affeldt-aist:edist_20261006

Conversation

@affeldt-aist

Copy link
Copy Markdown
Member
Motivation for this change

edist does not need normed_module.v to be defined anymore

fyi: @zstone1

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist added this to the 1.19.0 milestone Oct 6, 2026
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Oct 6, 2026
@affeldt-aist

Copy link
Copy Markdown
Member Author

(The conflict is on the changelog, can update anytime.)

@affeldt-aist

Copy link
Copy Markdown
Member Author

Since this PR does not change the API but just reduce the dependencies, I propose we merge provided the CI is green.

@affeldt-aist
affeldt-aist merged commit 23f0583 into math-comp:master Oct 9, 2026
70 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant