From 4231e694285c4050ccdf271ecdda69b4ce0bfed2 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 11 Mar 2024 20:17:40 -0400
Subject: [PATCH] chore: adapt to lean4#3654

---
 Std/Tactic/SqueezeScope.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Std/Tactic/SqueezeScope.lean b/Std/Tactic/SqueezeScope.lean
index 820618d84a..de1ed24aae 100644
--- a/Std/Tactic/SqueezeScope.lean
+++ b/Std/Tactic/SqueezeScope.lean
@@ -107,8 +107,9 @@ elab_rules : tactic
       | some mvarId => replaceMainGoal [mvarId]
       pure usedSimps
     | ``Parser.Tactic.dsimp => do
-      let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-      dsimpLocation' ctx (expandOptLocation stx[5])
+      let { ctx, simprocs, .. } ←
+        withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+      dsimpLocation' ctx simprocs (expandOptLocation stx[5])
     | _ => Elab.throwUnsupportedSyntax
     let a := a.getId; let x := x.getId
     squeezeScopes.modify fun map => Id.run do