Skip to content

Comments

fix #1849 (closure_subset -> closureS)#1857

Open
t6s wants to merge 2 commits intomath-comp:masterfrom
t6s:closureS
Open

fix #1849 (closure_subset -> closureS)#1857
t6s wants to merge 2 commits intomath-comp:masterfrom
t6s:closureS

Conversation

@t6s
Copy link
Member

@t6s t6s commented Feb 24, 2026

Motivation for this change
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

@t6s t6s added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Feb 24, 2026
@affeldt-aist affeldt-aist self-requested a review February 24, 2026 12:34
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A rebase and we're done! Thanks for noticing the naming issue.

@t6s
Copy link
Member Author

t6s commented Feb 24, 2026

rebased

@affeldt-aist
Copy link
Member

it looks like use is not supported by Coq 8.20:

#[deprecated(since="mathcomp-analysis 1.16.0", use=closureS)]
Definition closure_subset := closureS.

you can use note

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.

naming glitch at closure_subset

3 participants