Merge remote-tracking branch 'digama0/std_ns'

Lake/Build/Index.lean

@@ -15,7 +15,7 @@ Lake build functions, which is used by Lake to build any Lake build info.
 This module leverages the index to perform topologically-based recursive builds.
 -/
 
-open Std Lean
+open Lean
 namespace Lake
 
 /--

Lake/Build/Topological.lean

@@ -17,7 +17,6 @@ a build store.
 This is called a suspending scheduler in *Build systems à la carte*.
 -/
 
-open Std
 namespace Lake
 
 /-!

Lake/Config/Module.lean

@@ -7,7 +7,7 @@ import Lake.Build.Trace
 import Lake.Config.LeanLib
 
 namespace Lake
-open Std System
+open Lean System
 
 /-- A buildable Lean module of a `LeanLib`. -/
 structure Module where

Lake/Config/Package.lean

@@ -12,7 +12,7 @@ import Lake.Config.Dependency
 import Lake.Config.Script
 import Lake.Util.DRBMap
 
-open Std System Lean
+open System Lean
 
 namespace Lake
 

Lake/Load/Elab.lean

@@ -14,7 +14,7 @@ open Lean System
 deriving instance BEq, Hashable for Import
 
 /- Cache for the imported header environment of Lake configuration files. -/
-initialize importEnvCache : IO.Ref (Std.HashMap (List Import) Environment) ← IO.mkRef {}
+initialize importEnvCache : IO.Ref (HashMap (List Import) Environment) ← IO.mkRef {}
 
 /-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
 def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)

Lake/Load/Materialize.lean

@@ -7,7 +7,7 @@ import Lake.Util.Git
 import Lake.Load.Manifest
 import Lake.Config.Dependency
 
-open Std System Lean
+open System Lean
 
 namespace Lake
 

Lake/Util/DRBMap.lean

@@ -7,11 +7,11 @@ import Lean.Data.RBMap
 import Lake.Util.Compare
 
 namespace Lake
-open Std RBNode
+open Lean RBNode
 
 /-!
-This module includes a dependently typed adaption of the `Std.RBMap`
-defined in `Std.Data.RBMap` module of the Lean core. Most of the code is
+This module includes a dependently typed adaption of the `Lean.RBMap`
+defined in `Lean.Data.RBMap` module of the Lean core. Most of the code is
 copied directly from there with only minor edits.
 -/
 

Lake/Util/Name.lean

@@ -12,7 +12,7 @@ namespace Lake
 
 export Lean (Name NameMap)
 
-@[inline] def NameMap.empty : NameMap α := Std.RBMap.empty
+@[inline] def NameMap.empty : NameMap α := RBMap.empty
 
 instance : ForIn m (NameMap α) (Name × α) where
   forIn self init f := self.forIn init f

Lake/Util/StoreInsts.lean

@@ -7,7 +7,7 @@ import Lake.Util.DRBMap
 import Lake.Util.Family
 import Lake.Util.Store
 
-open Std Lean
+open Lean
 namespace Lake
 
 instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where