max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: do not save/restore cache at withNewMCtxDepth

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-02 11:17:20 -08:00
parent 770649ce1d
commit 798001af75
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Lean/Meta/Basic.lean
View file

@ -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`.