Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - fix(linear_algebra/matrix/determinant): remove coercions #9975

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - fix(linear_algebra/matrix/determinant): remove coercions #9975

wants to merge 1 commit into from

Conversation

eric-wieser
Copy link
Member

Open in Gitpod

@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. labels Oct 26, 2021
@robertylewis
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 Oct 26, 2021
bors bot pushed a commit that referenced this pull request Oct 26, 2021
@eric-wieser
fix(linear_algebra/matrix/determinant): remove coercions (#9975)
884546f
@bryangingechen
Copy link
Collaborator

bors crashed
bors r+

bors bot pushed a commit that referenced this pull request Oct 26, 2021
@eric-wieser
fix(linear_algebra/matrix/determinant): remove coercions (#9975)
11142d2
@bryangingechen
Copy link
Collaborator

Oh, actually the build failed before that: https://github.com/leanprover-community/mathlib/runs/4011245661?check_suite_focus=true
bors r-

@bors
Copy link

bors bot commented Oct 26, 2021

Canceled.

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Oct 26, 2021
@bryangingechen
Copy link
Collaborator

The failure is a timeout which seems like it might be unrelated. Feel free to put this back on the queue if you think it can go through.
bors d+

@bors
Copy link

bors bot commented Oct 26, 2021

✌️ eric-wieser 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 Oct 26, 2021
@eric-wieser
Copy link
Member Author

Timeout looks unrelated to me

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-author A reviewer has asked the author a question or requested changes labels Oct 26, 2021
bors bot pushed a commit that referenced this pull request Oct 26, 2021
@eric-wieser
fix(linear_algebra/matrix/determinant): remove coercions (#9975)
92e9078
@bors
Copy link

bors bot commented Oct 26, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix(linear_algebra/matrix/determinant): remove coercions [Merged by Bors] - fix(linear_algebra/matrix/determinant): remove coercions Oct 26, 2021
@bors bors bot closed this Oct 26, 2021
@bors bors bot deleted the eric-wieser/alg_hom.map_det-coercion branch October 26, 2021 21:02
ericrbg pushed a commit that referenced this pull request Nov 9, 2021
@eric-wieser @ericrbg
fix(linear_algebra/matrix/determinant): remove coercions (#9975)
f3c43c7
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. easy < 20s of review time. See the lifecycle page for guidelines. 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.
3 participants
@eric-wieser @robertylewis @bryangingechen