diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 479ec77e84..82c9e54cf9 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -14,7 +14,7 @@ open Server
 
 structure InteractiveHypothesis where
   /-- The user-friendly name for each hypothesis.
-  If anonymous then the name is inaccessible. -/
+  If anonymous then the name is inaccessible and hidden. -/
   names : Array Name
   fvarIds? : Option (Array FVarId)
   type : CodeWithInfos