diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index d1617f86cc..a13207a9cb 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -566,7 +566,7 @@ instance : MonadCache Expr Expr CheckAssignmentM := { private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData := do let ctx ← read - return m!" @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}" + return m!"{msg} @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}" @[specialize] def checkFVar (check : Expr → CheckAssignmentM Expr) (fvar : Expr) : CheckAssignmentM Expr := do let ctxMeta ← readThe Meta.Context