-
Notifications
You must be signed in to change notification settings - Fork 64
instead of lspace_master #1624
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
instead of lspace_master #1624
Conversation
|
The last commit renames the HB structure |
a7dcd80 to
7a253c7
Compare
CohenCyril
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the issues about the conjugate should be solved before merging.
theories/hoelder.v
Outdated
| Local Open Scope classical_set_scope. | ||
| Local Open Scope ereal_scope. | ||
|
|
||
| Definition conjugate := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| Definition conjugate := | |
| Definition hoelder_conjugate := |
527c36e to
98900a9
Compare
|
CI is green |
Motivation for this change
Closes #1506
I wasn't able to rebase, hence the new PR closing the old one. @hoheinzollern @CohenCyril @proux01 @t6s
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers