Skip to content

[Merged by Bors] - feat: port observe tactic from mathlib#3516

Closed
kim-em wants to merge 11 commits intomasterfrom
observe
Closed

[Merged by Bors] - feat: port observe tactic from mathlib#3516
kim-em wants to merge 11 commits intomasterfrom
observe

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Apr 19, 2023


Open in Gitpod

@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Apr 19, 2023
@kim-em kim-em requested a review from jcommelin April 19, 2023 09:53
@kim-em kim-em removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 19, 2023
@gebner gebner added the t-meta Tactics, attributes or user commands label Apr 19, 2023
Copy link
Copy Markdown
Member

@gebner gebner left a comment

Choose a reason for hiding this comment

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

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

✌️ 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.

@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Apr 20, 2023
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 20, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Apr 20, 2023
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 20, 2023

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 20, 2023

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 20, 2023

Gah.

bors merge

bors bot pushed a commit that referenced this pull request Apr 20, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 20, 2023

bors merge

bors bot pushed a commit that referenced this pull request Apr 20, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port observe tactic from mathlib [Merged by Bors] - feat: port observe tactic from mathlib Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the observe branch April 20, 2023 09:45
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
kim-em added a commit that referenced this pull request May 10, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants