From f0fa6dcbc5fe9d469e6dd45c34ed3ba2efbaddbf Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 6 Dec 2021 15:34:30 +0100
Subject: [PATCH] refactor: remove unnecessary Lean.Elab.Term imports

---
 src/Lean/Elab/Term.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 2bd5501138..7245e572e0 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -7,12 +7,9 @@ import Lean.ResolveName
 import Lean.Util.Sorry
 import Lean.Util.ReplaceExpr
 import Lean.Structure
-import Lean.Meta.ExprDefEq
 import Lean.Meta.AppBuilder
-import Lean.Meta.SynthInstance
 import Lean.Meta.CollectMVars
 import Lean.Meta.Coe
-import Lean.Meta.Tactic.Util
 import Lean.Hygiene
 import Lean.Util.RecDepth
 import Lean.Elab.Log