From 032dc4bc8f0ca5756f5903342172eb322fb722cb Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 14 Sep 2022 05:13:34 -0400 Subject: [PATCH] chore: move NameMap into a separate file --- Lake/Config/Dependency.lean | 2 +- Lake/Util/Name.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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