diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean index cce12ef257..e1ad319244 100644 --- a/tests/compiler/phashmap.lean +++ b/tests/compiler/phashmap.lean @@ -1,6 +1,6 @@ -import Init.Data.PersistentHashMap +import Std.Data.PersistentHashMap import Lean.Data.Format -open Lean PersistentHashMap +open Lean Std Std.PersistentHashMap abbrev Map := PersistentHashMap Nat Nat diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean index 31ddea6b5a..feda9d19d0 100644 --- a/tests/compiler/phashmap2.lean +++ b/tests/compiler/phashmap2.lean @@ -1,6 +1,6 @@ -import Init.Data.PersistentHashMap +import Std.Data.PersistentHashMap import Lean.Data.Format -open Lean PersistentHashMap +open Lean Std Std.PersistentHashMap abbrev Map := PersistentHashMap Nat Nat diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean index f525954b8a..b968f8f229 100644 --- a/tests/compiler/phashmap3.lean +++ b/tests/compiler/phashmap3.lean @@ -1,6 +1,6 @@ -import Init.Data.PersistentHashMap +import Std.Data.PersistentHashMap import Lean.Data.Format -open Lean PersistentHashMap +open Lean Std Std.PersistentHashMap abbrev Map := PersistentHashMap Nat Nat diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean index c335013e27..5d04564780 100644 --- a/tests/lean/phashmap_inst_coherence.lean +++ b/tests/lean/phashmap_inst_coherence.lean @@ -1,5 +1,5 @@ -import Init.Data.PersistentHashMap - +import Std.Data.PersistentHashMap +open Std def m : PersistentHashMap Nat Nat := let m : PersistentHashMap Nat Nat := {}; m.insert 1 1 diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean index b876aa82b2..27b7970d72 100644 --- a/tests/lean/run/sharecommon.lean +++ b/tests/lean/run/sharecommon.lean @@ -1,3 +1,5 @@ +import Std.ShareCommon +open Std def check (b : Bool) : ShareCommonT IO Unit := unless b $ throw $ IO.userError "check failed"