Skip to content

Commit e709b2f

Browse files
committed
perf: no need to specialize the debugging slow path
1 parent dd28f00 commit e709b2f

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Lean/Util/Trace.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ def addRawTrace (msg : MessageData) : m Unit := do
140140
let msg ← addMessageContext msg
141141
modifyTraces (·.push { ref, msg })
142142

143+
@[nospecialize]
143144
def addTrace (cls : Name) (msg : MessageData) : m Unit := do
144145
let ref ← getRef
145146
let msg ← addMessageContext msg

0 commit comments

Comments
 (0)