chore: fix imports (#8538)

leanprover-community · Nov 20, 2023 · f659b7b · f659b7b
1 parent 43b4712
commit f659b7b
Show file tree

Hide file tree

Showing 8 changed files with 9 additions and 8 deletions.
diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean
@@ -5,7 +5,7 @@ Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 
 import Mathlib.Algebra.Ring.Defs
-import Std.Data.Rat
+import Std.Data.Rat.Basic
 import Mathlib.Data.Rat.Init
 
 #align_import algebra.field.defs from "leanprover-community/mathlib"@"2651125b48fc5c170ab1111afd0817c903b1fc6c"

diff --git a/Mathlib/Data/HashMap.lean b/Mathlib/Data/HashMap.lean
@@ -8,8 +8,8 @@ nothing from the mathlib3 file `data.hash_map` is reflected here.
 The porting header is just here to mark that no further work on `data.hash_map` is desired.
 -/
 import Mathlib.Init.Align
-import Std.Data.HashMap
-import Std.Data.RBMap
+import Std.Data.HashMap.Basic
+import Std.Data.RBMap.Basic
 
 #align_import data.hash_map from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
 

diff --git a/Mathlib/Data/MLList/Dedup.lean b/Mathlib/Data/MLList/Dedup.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Std.Data.MLList.Basic
-import Std.Data.HashMap
+import Std.Data.HashMap.Basic
 
 /-!
 # Lazy deduplication of lazy lists

diff --git a/Mathlib/Data/Rat/Init.lean b/Mathlib/Data/Rat/Init.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Mathport.Rename
-import Std.Data.Rat
+import Std.Data.Rat.Basic
 
 #align_import data.rat.init from "leanprover-community/mathlib"@"f340f229b1f461aa1c8ee11e0a172d0a3b301a4a"
 

diff --git a/Mathlib/Data/Tree.lean b/Mathlib/Data/Tree.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 mathlib community. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Wojciech Nawrocki
 -/
-import Std.Data.RBMap
+import Std.Data.RBMap.Basic
 import Mathlib.Data.Num.Basic
 import Mathlib.Order.Basic
 import Mathlib.Init.Data.Ordering.Basic

diff --git a/Mathlib/Lean/Data/NameMap.lean b/Mathlib/Lean/Data/NameMap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster
 -/
 import Lean.Data.NameMap
-import Std.Data.RBMap
+import Std.Data.RBMap.Basic
 
 /-!
 # Additional functions on `Lean.NameMap`.

diff --git a/Mathlib/Lean/Name.lean b/Mathlib/Lean/Name.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Data.HashMap
+import Std.Data.HashMap.Basic
 import Mathlib.Lean.SMap
 import Mathlib.Lean.Expr.Basic
 

diff --git a/Mathlib/Util/LongNames.lean b/Mathlib/Util/LongNames.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import Std.Data.HashMap.WF
 import Mathlib.Lean.Name
 import Mathlib.Lean.Expr.Basic