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