Merge pull request #13 from leanprover/bump/v4.8.0

chore: move to v4.8.0-rc1
leanprover · May 2, 2024 · 94d8656 · 94d8656
2 parents 6b35946 + 76da07e
commit 94d8656
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Lean4CheckerTests/OpenPrivate.lean b/Lean4CheckerTests/OpenPrivate.lean
@@ -49,7 +49,7 @@ def elabOpenPrivateLike (ids : Array Ident) (tgts mods : Option (Array Ident))
   (f : (priv full user : Name) → CommandElabM Name) : CommandElabM Unit := do
   let mut names := NameSet.empty
   for tgt in tgts.getD #[] do
-    let n ← resolveGlobalConstNoOverloadWithInfo tgt
+    let n ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo tgt
     names ← Meta.collectPrivateIn n names
   for mod in mods.getD #[] do
     let some modIdx := (← getEnv).moduleIdxForModule? mod.getId

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.7.0
		leanprover/lean4:v4.8.0-rc1