From 5130da82a85cea2299e90111bccbb64cf9bb66ce Mon Sep 17 00:00:00 2001
From: Ed Ayers <EdAyers@users.noreply.github.com>
Date: Fri, 10 Jun 2022 12:41:18 -0400
Subject: [PATCH] doc: src/Lean/Widget/InteractiveGoal.lean

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
---
 src/Lean/Widget/InteractiveGoal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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