Skip to content

split measure.v#1719

Merged
affeldt-aist merged 2 commits intomath-comp:masterfrom
affeldt-aist:measure_20250918
Sep 24, 2025
Merged

split measure.v#1719
affeldt-aist merged 2 commits intomath-comp:masterfrom
affeldt-aist:measure_20250918

Conversation

@affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Sep 18, 2025

Motivation for this change

The changelog is almost complete (I just need to get through measure_structure.v).

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.14.0 milestone Sep 18, 2025
@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Sep 18, 2025
@affeldt-aist
Copy link
Member Author

comment addressed

@affeldt-aist
Copy link
Member Author

rebased, can be merged at any time ^_^

@affeldt-aist affeldt-aist merged commit fae5628 into math-comp:master Sep 24, 2025
82 of 84 checks passed
@affeldt-aist affeldt-aist mentioned this pull request Sep 24, 2025
yosakaon pushed a commit to yosakaon/analysis that referenced this pull request Dec 4, 2025
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.

2 participants