fix: withoutModifyingStateWithInfoAndMessagesImpl

Make sure it does not produced a corrupted `InfoTree`.
This commit is contained in:
Leonardo de Moura 2022-04-11 16:57:55 -07:00
parent 9f8dd99ccd
commit 3de607193f

View file

@ -305,7 +305,7 @@ def withoutModifyingElabMetaStateWithInfo (x : TermElabM α) : TermElabM α := d
private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : TermElabM α := do
let saved ← saveState
try
x
withSaveInfoContext x
finally
let s ← get
let saved := { saved with elab.infoState := s.infoState, elab.messages := s.messages }