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.
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
[Merged by Bors] - Deprecate allowing auto-replacement #10302
Conversation
bors r+
is the same in both cases). |
Following [these](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Thank.20you.20for.20the.20deprecation.20warnings!/near/420078161) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/machineApplicableDeprecated.20tag.20attribute/near/397630551) discussions, I realised that my deprecation script produced a deprecation syntax that did not allow for auto-replacement in Sébastien's #10185. This PR fixes the deprecation statements, allowing self-correction: 119 times I replaced `@[deprecated xxx] --> @[deprecated]`.
@sgouezel I think that it is a quirk of |
Since we have a working solution, I'm not sure it's worth your time looking into the details of the implementation. |
Pull request successfully merged into master. Build succeeded: |
Following [these](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Thank.20you.20for.20the.20deprecation.20warnings!/near/420078161) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/machineApplicableDeprecated.20tag.20attribute/near/397630551) discussions, I realised that my deprecation script produced a deprecation syntax that did not allow for auto-replacement in Sébastien's #10185. This PR fixes the deprecation statements, allowing self-correction: 119 times I replaced `@[deprecated xxx] --> @[deprecated]`.
Following [these](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Thank.20you.20for.20the.20deprecation.20warnings!/near/420078161) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/machineApplicableDeprecated.20tag.20attribute/near/397630551) discussions, I realised that my deprecation script produced a deprecation syntax that did not allow for auto-replacement in Sébastien's #10185. This PR fixes the deprecation statements, allowing self-correction: 119 times I replaced `@[deprecated xxx] --> @[deprecated]`.
Following these Zulip discussions, I realised that my deprecation script produced a deprecation syntax that did not allow for auto-replacement in Sébastien's #10185.
This PR fixes the deprecation statements, allowing self-correction: 119 times I replaced
@[deprecated xxx] --> @[deprecated]
.