diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index b69b3d2712..d94ace5f20 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -30,7 +30,7 @@ structure InteractiveGoal where
   goalPrefix : String
   /-- Identifies the goal (ie with the unique
   name of the MVar that it is a goal for.)
-  [todo] what should the key be for a term goal?-/
+  This is none when we are showing a term goal. -/
   mvarId? : Option MVarId := none
   deriving Inhabited, RpcEncoding