diff --git a/Lake/Config/Dependency.lean b/Lake/Config/Dependency.lean index 4553132442..b92d07b7e2 100644 --- a/Lake/Config/Dependency.lean +++ b/Lake/Config/Dependency.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ -import Lean.Data.Name +import Lean.Data.NameMap namespace Lake open Lean System diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index f2c294c659..2641a0363b 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lean.Data.Name +import Lean.Data.NameMap import Lake.Util.Compare open Lean