From feda5e746fa4de5360a5d2b21e884445fbce83cc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Aug 2020 11:50:08 -0700 Subject: [PATCH] chore: improve error message --- src/Lean/Meta/Tactic/Subst.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index e99288a326..b31de873a3 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -103,6 +103,7 @@ withMVarContext mvarId $ do "invalid equality proof, it is not of the form " ++ (if symm then "(t = x)" else "(x = t)") ++ indentExpr hLocalDecl.type + ++ Format.line ++ "after WHNF, variable expected, but obtained" ++ indentExpr a def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId := withMVarContext mvarId $ do