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