Kim Morrison f70b7e5722 feat: @[deprecated] requires a replacement identifier or message, and a since field (#6112) ... This PR makes stricter requirements for the `@[deprecated]` attribute, requiring either a replacement identifier as `@[deprecated bar]` or suggestion text `@[deprecated "Past its use by date"]`, and also requires a `since := "..."` field.		2024-11-26 08:45:54 +00:00
..
Basic.lean	chore: deprecate := variants of inductive and structure (#5542)	2024-10-11 05:54:18 +00:00
Builtin.lean	chore: add missing copyright headers (#3411)	2024-02-20 01:49:55 +00:00
ConstructorAsVariable.lean	perf: do not lint unused variables defined in tactics by default (#5338)	2024-10-17 09:55:11 +00:00
Deprecated.lean	feat: @[deprecated] requires a replacement identifier or message, and a since field (#6112)	2024-11-26 08:45:54 +00:00
MissingDocs.lean	chore: switch to Std.HashMap and Std.HashSet almost everywhere	2024-08-07 18:24:42 +02:00
Omit.lean	feat: omit (#5000)	2024-08-21 13:22:34 +00:00
UnusedVariables.lean	feat: structure auto-completion & partial InfoTrees	2024-11-19 09:26:58 +01:00
Util.lean	feat: improve unused section variable warning (#5036)	2024-08-22 10:18:09 +00:00