From 3de607193f9273fa29105a34d177b219f0bc44d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Apr 2022 16:57:55 -0700
Subject: [PATCH] fix: `withoutModifyingStateWithInfoAndMessagesImpl`

Make sure it does not produced a corrupted `InfoTree`.
---
 src/Lean/Elab/Term.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 19e4bbddcc..2af540ea84 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -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 }