From dc77c45787b4ef1d7656eebbbb7fb3ec0599bcbe Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 Jan 2021 13:11:30 +0100 Subject: [PATCH] fix: mvar check trace message --- src/Lean/Meta/ExprDefEq.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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