From 21262e5dca563ab2cbcfb911beb7a4dc8b646607 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 11:14:25 -0400 Subject: [PATCH] chore: move Bootstrap.Data -> Lean.Data --- Lake/Util/DRBMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Util/DRBMap.lean b/Lake/Util/DRBMap.lean index 21cf85e9e2..ef64f4f1d4 100644 --- a/Lake/Util/DRBMap.lean +++ b/Lake/Util/DRBMap.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mac Malone -/ -import Bootstrap.Data.RBMap +import Lean.Data.RBMap import Lake.Util.Compare namespace Lake