chore: move to v4.9.0-rc1 (#44)

* chore: adaptations for nightly-2024-05-09 (#43) * move to v4.9.0-rc1
leanprover-community · Jun 7, 2024 · a7bfa63 · a7bfa63
1 parent 5315667
commit a7bfa63
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
@@ -495,7 +495,7 @@ def Impl.macro (t : Syntax) (expectedType : Expr) : TermElabM Expr := do
       withProcessPostponed do withSynthesize do
       let t ← Term.elabTerm t lastDecl.type
       let t ← ensureHasType lastDecl.type t
-      synthesizeSyntheticMVars (mayPostpone := false)
+      synthesizeSyntheticMVars (postpone := .no)
       if (← logUnassignedUsingErrorInfos (← getMVars t)) then
         throwAbortTerm
       lastId.assign t

diff --git a/Qq/Match.lean b/Qq/Match.lean
@@ -172,7 +172,7 @@ def elabPat (pat : Term) (lctx : LocalContext) (localInsts : LocalInstances) (ty
           let (pat, patVars) ← getPatVars pat #[]
           let pat ← Lean.Elab.Term.elabTerm pat ty
           let pat ← ensureHasType ty pat
-          synthesizeSyntheticMVars false
+          synthesizeSyntheticMVars (postpone := .no)
           let pat ← instantiateMVars pat
 
           let mctx ← getMCtx

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