diff --git a/Lake/Attributes.lean b/Lake/Attributes.lean index 3d59d3fe5e..d9fac00590 100644 --- a/Lake/Attributes.lean +++ b/Lake/Attributes.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lean +import Lean.Attributes open Lean namespace Lake diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean index 67a72f8503..b7dbd97d1a 100644 --- a/Lake/LeanConfig.lean +++ b/Lake/LeanConfig.lean @@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lean +import Lean.Elab.Frontend import Lake.Package import Lake.Attributes