chore: adapt to lean4#3654

thorimur · Mar 12, 2024 · 4231e69 · 4231e69
1 parent f3447c3
commit 4231e69
Showing 1 changed file with 3 additions and 2 deletions.
diff --git 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