fix: remove unused trace.Elab.syntax option

2026-03-27 15:24:17 +00:00 · 2024-04-08 17:28:51 +02:00
1 changed files with 0 additions and 3 deletions
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -442,7 +442,4 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
  | some str => return mkAtomFrom stx str
  | none     => Macro.throwUnsupported

-builtin_initialize
-  registerTraceClass `Elab.syntax
-
 end Lean.Elab.Command