In the Coq stdlib index, about 65% of the entries are binders. Similarly, in a randomly chosen project of mine, the binders are 45% of the entries in the index.
It's likely that nobody ever consults the binder index, for any reason. Yet, I can't find an easy way to disable binder index generation and listing... Worth an issue, or is this well known?
OK, I'm tempted to just do a PR purging the binder index from everywhere, but hopefully Hugo can suggest something less radical
you should do it
Hugo is pretty busy AFAIK
OK, I guess he might just do a :thumbs_up: or :thumbs_down: on the PR if he's still monitoring coqdoc stuff
Copying my comment on #13155: I did not realize that adding links for binders would create an index. I don't think it is useful indeed. If there is a PR for removing it, it is a :+1:.
OK, I will put this on my plate then, hopefully a PR in 1-2 days.
Last updated: Feb 06 2023 at 00:03 UTC