From 7a964ecbea90495e8d4ec06c4880b0690995db3d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 May 2020 16:33:03 -0700
Subject: [PATCH] chore: register `Elab.struct trace class

---
 src/Init/Lean/Elab/StructInst.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Lean/Elab/StructInst.lean b/src/Init/Lean/Elab/StructInst.lean
index 45c3e58b87..eedf81fed7 100644
--- a/src/Init/Lean/Elab/StructInst.lean
+++ b/src/Init/Lean/Elab/StructInst.lean
@@ -787,6 +787,10 @@ fun stx expectedType? => do
       | some _,        _                        => throwError stx ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
       | _,             _                        => elabStructInstAux stx expectedType? sourceView
 
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Elab.struct;
+pure ()
+
 end StructInst
 end Term
 end Elab