From fcb1616c20dc1b3d3be1336b843ba675cdaf6446 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 16 Jan 2021 19:45:45 +0100
Subject: [PATCH] chore: reduce dependencies

---
 src/Lean/Server/InfoUtils.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index f5f7ca223a..c81742b9d4 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Wojciech Nawrocki
 -/
-import Lean.Elab
+import Lean.Elab.InfoTree
 
 namespace Lean.Elab