From 43bc429abf49526b7b794d2fe076f961841a8fc9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Sep 2020 15:18:20 -0700
Subject: [PATCH] fix: typo

---
 src/Lean/Meta/Tactic/Replace.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean
index 8a7999b2b8..ed953a874e 100644
--- a/src/Lean/Meta/Tactic/Replace.lean
+++ b/src/Lean/Meta/Tactic/Replace.lean
@@ -25,8 +25,8 @@ withMVarContext mvarId do
   u        ← getLevel target;
   eq       ← mkEq target targetNew;
   newProof ← mkExpectedTypeHint eqProof eq;
-  let newVal := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew];
-  assignExprMVar mvarId mvarNew;
+  let val  := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew];
+  assignExprMVar mvarId val;
   pure mvarNew.mvarId!
 
 /--