From 51d1ed733e5bdcd8eaf9988152e72538e2f23474 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 14 Feb 2024 19:59:25 -0500
Subject: [PATCH] chore: update to Lean v4.6.0-rc1

---
 Alloy/Util/Command.lean | 4 ++--
 lean-toolchain          | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Alloy/Util/Command.lean b/Alloy/Util/Command.lean
index 8e3017f..dce5984 100644
--- 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
index 8901863..8ca3fcc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.3.0
+leanprover/lean4:4.6.0-rc1