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