diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 73b328ab22..8d5b6bef0e 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1811,7 +1811,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD builtin_initialize registerTraceClass `Meta.isDefEq registerTraceClass `Meta.isDefEq.stuck - registerTraceClass `Meta.isDefEq.stuck.mvar (inherited := true) + registerTraceClass `Meta.isDefEq.stuckMVar (inherited := true) registerTraceClass `Meta.isDefEq.cache registerTraceClass `Meta.isDefEq.foApprox (inherited := true) registerTraceClass `Meta.isDefEq.onFailure (inherited := true)