diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 878bdb99df..be4ea16cca 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich import Lean.Data.Trie import Lean.Data.Position import Lean.Syntax -import Lean.ToExpr import Lean.Environment import Lean.Message