From f4bae4cd2a8ee0fa595ab417932a790e15d8cb5a Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 01:03:08 -0400 Subject: [PATCH] chore: move Std -> Bootstrap --- 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 182f970417..21cf85e9e2 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 Std.Data.RBMap +import Bootstrap.Data.RBMap import Lake.Util.Compare namespace Lake