adaptations for v4.8.0

leanprover · Mar 18, 2024 · 4d2ed60 · 4d2ed60
1 parent 9b652c8
commit 4d2ed60
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-rc1
+leanprover/lean4:nightly-2024-03-16
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.7.0-rc1
		leanprover/lean4:nightly-2024-03-16