Skip to content

[Merged by Bors] - feat: port ac_change tactic#5869

Closed
Komyyy wants to merge 5 commits intomasterfrom
Komyyy/ac_change
Closed

[Merged by Bors] - feat: port ac_change tactic#5869
Komyyy wants to merge 5 commits intomasterfrom
Komyyy/ac_change

Conversation

@Komyyy
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy commented Jul 13, 2023

Just a macro.

Open in Gitpod

@Komyyy Komyyy added awaiting-review t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. mathlib-port This is a port of a theory file from mathlib. labels Jul 13, 2023
@Komyyy Komyyy mentioned this pull request Jul 13, 2023
Open
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 13, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 14, 2023
@Komyyy Komyyy added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 14, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 14, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 18, 2023
@Komyyy Komyyy removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 22, 2023
@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 4, 2023

I pushed what I think is an improvement to this branch, please check you agree @Komyyy

@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented Aug 5, 2023

@alexjbest
Nice change, thank you!

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 5, 2023

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 5, 2023

🚀 Pull request has been placed on the maintainer queue by alexjbest.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Aug 8, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 8, 2023
bors bot pushed a commit that referenced this pull request Aug 8, 2023
@Komyyy @alexjbest
feat: port ac_change tactic (#5869)
1c91df4 
Just a macro.



Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Aug 8, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port ac_change tactic [Merged by Bors] - feat: port ac_change tactic Aug 8, 2023
@bors bors bot closed this Aug 8, 2023
@bors bors bot deleted the Komyyy/ac_change branch August 8, 2023 16:37
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@Komyyy @alexjbest @kim-em
feat: port ac_change tactic (#5869)
8106d1b 
Just a macro.



Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
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

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Komyyy @alexjbest @j-loreaux @kim-em