From be06ce5fecd92a3ee171492d2548352bdf4f6fb0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jul 2020 16:45:51 -0700
Subject: [PATCH] chore: update TODO list

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

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index f2622b671e..5105b4cf39 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -474,8 +474,9 @@ withDeclId declId $ fun name => do
   let ref := declId;
   addDecl ref r.decl;
   addProjections ref declName r.projInfos isClass;
-  -- TODO: add auxiliary definitions
+  -- TODO: add auxiliary definitions recOn and casesOn
   -- TODO: register default values
+  -- TODO: add coercions
   pure ()
 
 end Command