From 401de35b6cdc2d0079b74b9e45204db36c8cead5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Jun 2019 10:53:51 -0700 Subject: [PATCH] chore(library/init/lean/parser/parser): remove unnecessary import It turns out we don't need evalConst for implementing `builtinParsers`. --- library/init/lean/parser/parser.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 4f568f86d7..2b8aabda33 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -9,7 +9,6 @@ import init.lean.syntax import init.lean.toexpr import init.lean.environment import init.lean.attributes -import init.lean.evalconst import init.lean.parser.trie import init.lean.parser.identifier import init.lean.compiler.initattr