chore: update to Lean v4.6.0-rc1

tydeu · Feb 15, 2024 · 5ae885f · 5ae885f
1 parent d364c8c
commit 5ae885f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Alloy/Util/Command.lean b/Alloy/Util/Command.lean
@@ -13,7 +13,7 @@ open Lean Elab Command
   .node (.ofCommandInfo { elaborator, stx }) trees
 
 /-- Create context info for the info tree from the current state of command elaboration.  -/
-def mkCommandElabContextInfo : CommandElabM ContextInfo := do
+def mkCommandElabContextInfo : CommandElabM CommandContextInfo := do
   let ctx ← read; let s ← get; let scope := s.scopes.head!
   return  {
     env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace,
@@ -22,7 +22,7 @@ def mkCommandElabContextInfo : CommandElabM ContextInfo := do
 
 /-- Create an info tree for an elaborator with the current command elaboration context. -/
 @[inline] def mkCommandElabInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do
-  return .context (← mkCommandElabContextInfo) (mkElabInfoTree elaborator stx trees)
+  return .context (.commandCtx (← mkCommandElabContextInfo)) (mkElabInfoTree elaborator stx trees)
 
 /-- Adapted from the private `elabCommandUsing` definition in `Lean.Elab.Command`. -/
 def elabCommandUsing (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Bool

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.3.0
+leanprover/lean4:4.6.0-rc1