From 2fda7f4f9f2e7d5940ba553a1dc46462e28cf613 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Oct 2020 19:12:08 -0700
Subject: [PATCH] chore: add `TODO`

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

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index fc95262c65..35525b7344 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -934,6 +934,8 @@ unit ← `(PUnit.unit);
 let unit := unit.copyInfo ref;
 pure $ mkReturn ref unit
 
+-- TODO: we must expand macros occurring in patterns before invoking getPatternVars
+
 partial def doSeqToCode : List Syntax → M CodeBlock
 | [] => do ctx ← read; mkReturnUnit ctx.ref
 | doElem::doElems => withRef doElem do