From 3d4bc9f99121b8caab1ed6444cc774d512c267cf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Feb 2021 18:31:28 -0800
Subject: [PATCH] chore: provide `ambient` monad to `forIn`

---
 src/Lean/Elab/Do.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index b6d4765c9f..88cfb13142 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1354,7 +1354,7 @@ mutual
       let uvarsTuple ← liftMacroM do mkTuple (← uvars.mapM mkIdentFromRef)
       if hasReturn forInBodyCodeBlock.code then
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ← `(forIn $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
+        let forInTerm ← `(forIn (m := $((← read).m)) $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
         let auxDo ← `(do let r ← $forInTerm:term;
                          $uvarsTuple:term := r.2;
                          match r.1 with
@@ -1363,7 +1363,7 @@ mutual
         doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
       else
         let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
-        let forInTerm ← `(forIn $(xs) $uvarsTuple fun $x r => $forInBody)
+        let forInTerm ← `(forIn (m := $((← read).m)) $(xs) $uvarsTuple fun $x r => $forInBody)
         if doElems.isEmpty then
           let auxDo ← `(do let r ← $forInTerm:term;
                            $uvarsTuple:term := r;