cdd982a030
This PR adds a `deprecated_syntax` command that marks syntax kinds as deprecated. When deprecated syntax is elaborated (in terms, tactics, or commands), a linter warning is emitted. The warning is also emitted during quotation precheck when a macro definition uses deprecated syntax in its expansion. The `deprecated_syntax` command takes a syntax node kind, an optional message, and a `(since := "...")` clause. Deprecation warnings correctly attribute the warning to macro call sites when the deprecated syntax is produced by macro expansion, including through nested macro chains. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> |
||
|---|---|---|
| .. | ||
| src | ||
| stdlib | ||