chore: force cmdliner doc argument to be explicit

[Alizter]

A common issue we have is undocumented arguments. It doesn't help that cmdliner hides the doc argument making it easy to miss. This is a common point of confusion for users #12722. In order to aid this we make the argument explicit. This makes it more apparent what is documented and what isn't.

[Leonidas-from-XIV]

I think it's a reasonable change. Maybe it would be good to add a comment in places where ~doc:None exists with the TODO of adding documentation?

[Alizter]

I would regard any ~doc:None as a TODO for documentation from this point on. Leaving things undocumented only causes confusion for users, so we don't have a good reason to leave doc as None.

[Leonidas-from-XIV]

Yeah, but it is hard to search for and hard to know for readers so having a (* CR-later: document argument *) or so would be nice as it signals to readers of the source that documentation is to be added and is not intentionally undocumented.

[Leonidas-from-XIV]

Thanks! I think except for the boot/libs.ml change this is good to go.

[Alizter]

There are around 20 arguments undocumented. I think many of these have a sensible documentation, I'll try to get them done eventually. (After this PR)