From f3de32cbf4b91032cf61c30339cd0362c3f88487 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Feb 2020 17:28:31 -0800
Subject: [PATCH] chore: helper method

---
 src/Init/Lean/Elab/Term.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 000824bc91..de1ccd3c54 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -301,6 +301,10 @@ def getDecLevel (ref : Syntax) (type : Expr) : TermElabM Level := do
 u ← getLevel ref type;
 decLevel ref u
 
+@[inline] def savingMCtx {α} (x : TermElabM α) : TermElabM α := do
+mctx ← getMCtx;
+finally x (modify $ fun s => { mctx := mctx, .. s })
+
 def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
 fun ctx s =>
   match (x { .. ctx }).run { .. s } with