From eef413cec8973672c80ea4e27838a64403e50cd3 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Sat, 10 Jul 2021 16:38:06 -0700
Subject: [PATCH] chore: unused binding in FromToJson

---
 src/Lean/Elab/Deriving/FromToJson.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index a986383e3b..7c4149c207 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -132,7 +132,6 @@ where
           let localDecl ← getLocalDecl x.fvarId!
           if !localDecl.userName.hasMacroScopes then
             userNames := userNames.push localDecl.userName
-          let xTy ← inferType x
           let a := mkIdent (← mkFreshUserName `a)
           identNames := identNames.push a
         let jsonAccess ← identNames.mapIdxM (fun idx _ => `(jsons[$(quote idx.val)]))