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