From 798001af75780e730ce74e5a70422ce05aa857a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2019 11:17:20 -0800
Subject: [PATCH] refactor: do not save/restore cache at `withNewMCtxDepth`

---
 src/Init/Lean/Meta/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index c786a6d54c..5dda5df5a0 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -709,10 +709,9 @@ do fvarId ← mkFreshId;
   and restore saved data. -/
 @[inline] def withNewMCtxDepth {α} (x : MetaM α) : MetaM α :=
 do s ← get;
-   let savedCache := s.cache;
    let savedMCtx  := s.mctx;
    modify $ fun s => { mctx := s.mctx.incDepth, .. s };
-   finally x (modify $ fun s => { cache := savedCache, mctx := savedMCtx, .. s })
+   finally x (modify $ fun s => { mctx := savedMCtx, .. s })
 
 /--
   Execute `x` using the given metavariable `LocalContext` and `LocalInstances`.