From 657879fcaa0811da82ce90b0a769cca6a065221d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Jun 2020 11:58:49 -0700 Subject: [PATCH] chore: fix tests --- tests/compiler/phashmap.lean | 4 ++-- tests/compiler/phashmap2.lean | 4 ++-- tests/compiler/phashmap3.lean | 4 ++-- tests/lean/phashmap_inst_coherence.lean | 4 ++-- tests/lean/run/sharecommon.lean | 2 ++ 5 files changed, 10 insertions(+), 8 deletions(-) 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"