fix: checkpoint

This commit is contained in:
Leonardo de Moura 2022-04-01 05:52:09 -07:00
parent 9fdb7429d4
commit 92382ea47b

View file

@ -34,6 +34,7 @@ private def findCache? (cacheRef : IO.Ref Cache) (mvarId : MVarId) (stx : Syntax
let mvarId ← getMainGoal
match (← findCache? cacheRef mvarId stx[1]) with
| some s =>
cacheRef.modify fun { pre, post } => { pre, post := post.insert mvarId s }
set s.core
set s.meta
set s.term