From dddf9e8a3fb9bdaa56d8d9c36b29048999b404bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Oct 2022 08:35:47 -0700
Subject: [PATCH] chore: remove leftover comment

---
 src/Lean/Elab/Term.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 64cde873eb..5ef159ea97 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -226,11 +226,6 @@ abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
 /-
 Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 whole monad stack at every use site. May eventually be covered by `deriving`.
-
-TODO: this trick does not work in the old/new code generators anymore.
-TODO: figure out a way to instruct the compiler to optimize this code once,
-and then lambda lift all methods once. Perhaps, we should do it whenever the
-instance is marked as always_inline.
 -/
 @[always_inline]
 instance : Monad TermElabM :=