diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean index 2941a22493..4cf353e6d4 100644 --- a/src/Init/Lean/Elab/Util.lean +++ b/src/Init/Lean/Elab/Util.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Init.Lean.Util.Trace import Init.Lean.Parser namespace Lean @@ -65,5 +66,8 @@ do ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvE }; pure { ext := ext, attr := attrImpl, kind := kind } +@[init] private def regTraceClasses : IO Unit := +registerTraceClass `Elab + end Elab end Lean