also reset dsimpCache

Author: JovanGerb

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -721,7 +721,7 @@ partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
 def simpApp (e : Expr) : SimpM Result := do
   if isOfNatNatLit e || isOfScientificLit e then
     -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
-    withFreshCache <| withInNumLit <| congr e
+    withFreshCache <| withFreshDSimpCache <| withInNumLit <| congr e
   else if isCharLit e then
     return { expr := e }
   else if isNonDepLetFun e then

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -483,6 +483,14 @@ Save current cache, reset it, execute `x`, and then restore original cache.
   modify fun s => { s with cache := {} }
   try x finally modify fun s => { s with cache := cacheSaved }
 
+/--
+Save current `dsimpCache`, reset it, execute `x`, and then resotre original cache.
+-/
+@[inline] def withFreshDSimpCache (x : SimpM α) : SimpM α := do
+  let cacheSaved := (← get).dsimpCache
+  modify fun s => { s with dsimpCache := {} }
+  try x finally modify fun s => { s with dsimpCache := cacheSaved }
+
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (wellBehavedDischarge : Bool) (x : SimpM α) : SimpM α :=
   withFreshCache <|
   withReader (fun r => { MethodsRef.toMethods r with discharge?, wellBehavedDischarge }.toMethodsRef) x