chore: simproc PR changes (#496)

See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Feb 5, 2024 · 89fe00d · 89fe00d
1 parent 19abd0c
commit 89fe00d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Std/Lean/Meta/Simp.lean b/Std/Lean/Meta/Simp.lean
@@ -58,7 +58,7 @@ def mkSimpContext' (simpTheorems : SimpTheorems) (stx : Syntax) (eraseLocal : Bo
   let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
     config       := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
-  }
+  } simprocs
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else