From a4a3f7d6a540ae456f1ef28f3c3294c651606414 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 9 Feb 2020 16:47:14 -0800
Subject: [PATCH] fix: typo

---
 src/Init/Lean/Meta/Tactic/Clear.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/Tactic/Clear.lean b/src/Init/Lean/Meta/Tactic/Clear.lean
index fd9267f5f6..330caf0a6b 100644
--- a/src/Init/Lean/Meta/Tactic/Clear.lean
+++ b/src/Init/Lean/Meta/Tactic/Clear.lean
@@ -20,7 +20,7 @@ withMVarContext mvarId $ do
   lctx.forM $ fun localDecl =>
     unless (localDecl.fvarId == fvarId) $
       when (mctx.localDeclDependsOn localDecl fvarId) $
-        throwTacticEx `clear mvarId ("variable '" ++ localDecl.value ++ "' depends on '" ++ mkFVar fvarId ++ "'");
+        throwTacticEx `clear mvarId ("variable '" ++ localDecl.toExpr ++ "' depends on '" ++ mkFVar fvarId ++ "'");
   mvarDecl ← getMVarDecl mvarId;
   when (mctx.exprDependsOn mvarDecl.type fvarId) $
     throwTacticEx `clear mvarId ("taget depends on '" ++ mkFVar fvarId ++ "'");