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] - chore(data/mv_polynomial): use bundled homs #3595

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - chore(data/mv_polynomial): use bundled homs #3595

wants to merge 16 commits into from

Conversation

semorrison
Copy link
Collaborator

I've done a lot of the scut work, but there are still about half a dozen broken proofs, if anyone would like to take a bash at them!

@semorrison semorrison added help-wanted The author needs attention to resolve issues WIP Work in progress labels Jul 28, 2020
@semorrison
Copy link
Collaborator Author

Oops, I seem to have lost the relevant commit.

@semorrison semorrison closed this Jul 28, 2020
@semorrison semorrison reopened this Jul 28, 2020
@semorrison
Copy link
Collaborator Author

🎉

@semorrison semorrison added awaiting-review The author would like community review of the PR and removed WIP Work in progress help-wanted The author needs attention to resolve issues labels Jul 28, 2020
@semorrison semorrison changed the title chore(data/mv_polynomial): attempting use bundled homs chore(data/mv_polynomial): use bundled homs Jul 28, 2020
@ChrisHughes24
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 28, 2020
bors bot pushed a commit that referenced this pull request Jul 28, 2020
@semorrison @jcommelin
chore(data/mv_polynomial): use bundled homs (#3595)
4ae8752 
I've done a lot of the scut work, but there are still about half a dozen broken proofs, if anyone would like to take a bash at them!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Jul 28, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(data/mv_polynomial): use bundled homs [Merged by Bors] - chore(data/mv_polynomial): use bundled homs Jul 28, 2020
@bors bors bot closed this Jul 28, 2020
@bors bors bot deleted the mv_polynomial_bundling branch July 28, 2020 20:45
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
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
3 participants
@semorrison @ChrisHughes24 @jcommelin