From 1f2f44dc9fd22dcab87d91cdfbb88c592e8409e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Apr 2018 13:42:18 -0700 Subject: [PATCH] chore(library/init/lean/parser/macro): fix `import` --- library/init/lean/parser/macro.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/parser/macro.lean b/library/init/lean/parser/macro.lean index 4edf821128..ca36565656 100644 --- a/library/init/lean/parser/macro.lean +++ b/library/init/lean/parser/macro.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich -/ prelude -import init.parser.move -import init.parser.syntax +import init.lean.parser.move +import init.lean.parser.syntax import init.meta.well_founded_tactics namespace lean.parser