Skip to content

[Merged by Bors] - chore: Deprecated aliases for Rat.cast_natCast, Rat.cast_intCast#11636

Closed
YaelDillies wants to merge 1 commit intomasterfrom
deprecate_rat_cast_nat_cast
Closed

[Merged by Bors] - chore: Deprecated aliases for Rat.cast_natCast, Rat.cast_intCast#11636
YaelDillies wants to merge 1 commit intomasterfrom
deprecate_rat_cast_nat_cast

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Mar 24, 2024

These were moved in #11552.


Open in Gitpod

@YaelDillies YaelDillies added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. labels Mar 24, 2024
@YaelDillies YaelDillies requested a review from eric-wieser March 24, 2024 21:03
@fpvandoorn
Copy link
Copy Markdown
Member

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 24, 2024

✌️ YaelDillies 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 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Mar 24, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor Author

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 24, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 24, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Deprecated aliases for Rat.cast_natCast, Rat.cast_intCast [Merged by Bors] - chore: Deprecated aliases for Rat.cast_natCast, Rat.cast_intCast Mar 24, 2024
@mathlib-bors mathlib-bors bot closed this Mar 24, 2024
@mathlib-bors mathlib-bors bot deleted the deprecate_rat_cast_nat_cast branch March 24, 2024 22:59
xgenereux pushed a commit that referenced this pull request Mar 25, 2024
utensil pushed a commit that referenced this pull request Mar 26, 2024
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
callesonne pushed a commit that referenced this pull request Apr 22, 2024
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). easy < 20s of review time. See the lifecycle page for guidelines.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants