Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 #17424

Closed
wants to merge 211 commits into from
Closed

[Merged by Bors] - refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 #17424

wants to merge 211 commits into from

Conversation

semorrison
Copy link
Collaborator

Open in Gitpod

urkud and others added 30 commits October 28, 2022 07:40
@urkud
Snapshot
798ae5a
@urkud
Fix
8b95538
@urkud
Fix
8ff0da7
@urkud
Snapshot
9a837ac
@semorrison
chore(data/nat/gcd/basic): remove spurious imports
d580e6f
@semorrison
chore(algebra/group_power/basic): reduce imports
2b2a498
@semorrison
chore(data/nat/cast): remove spurious imports
f07facb
@semorrison
initial split
4569ec7
@semorrison
chore(logic/small): split to reduce imports
3cc3ae2
@semorrison
fix
aa63a9c
@semorrison
chore(category_theory/category/preorder): split material on galois co…
e48f807 
…nnections
@semorrison
fix
d11ffde
@semorrison
move stuff
d99d8d2
@semorrison
cleanup
1c37bc5
@semorrison
cleanup
2c0085e
@semorrison
further reorg
aa070a6
@semorrison
cleanup
c83b897
@semorrison
module doc
0a4f3cf
@semorrison
.
f0ff047
@YaelDillies
move(data/set/pointwise/interval): Sanitise imports
5434717
@semorrison
hmm
da4e5f1
@semorrison
.
a253144
@semorrison
fix
3521db4
@semorrison
fix
1df9ed1
@semorrison
Merge remote-tracking branch 'origin/master' into data_nat_gcd_basic_…
30f5b6e 
…imports
@semorrison
fix
1dbbb26
@semorrison
chore(algebra/order/field): don't import finiteness hierarchy
65b5ab9
@semorrison
oops
3128062
@semorrison
make use of new directory
5a7dc1c
@semorrison
cleanup import
7c3d071
@jcommelin
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Nov 8, 2022

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Nov 8, 2022
@semorrison semorrison changed the title refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 Nov 8, 2022
@semorrison semorrison removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 8, 2022
@semorrison
Copy link
Collaborator Author

bors merge p=10

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Nov 8, 2022
bors bot pushed a commit that referenced this pull request Nov 8, 2022
@semorrison @urkud @YaelDillies
refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #…
88dbb36 
…17421 #17422 #17423 #17427 #17430 (#17424)




Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Nov 8, 2022

Canceled.

@semorrison
Copy link
Collaborator Author

bors merge p=10

bors bot pushed a commit that referenced this pull request Nov 8, 2022
@semorrison @urkud @YaelDillies
refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #…
c420411 
…17421 #17422 #17423 #17427 #17430 (#17424)




Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Nov 8, 2022

Build failed:

@semorrison
Copy link
Collaborator Author

bors merge p=10

bors bot pushed a commit that referenced this pull request Nov 8, 2022
@semorrison @urkud @YaelDillies
refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #…
47b5151 
…17421 #17422 #17423 #17427 #17430 (#17424)




Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bors
Copy link

bors bot commented Nov 9, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 [Merged by Bors] - refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 Nov 9, 2022
@bors bors bot closed this Nov 9, 2022
@bors bors bot deleted the sup5 branch November 9, 2022 00:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@semorrison @jcommelin @urkud @YaelDillies @PatrickMassot @fpvandoorn