Be more strict about doc comments

Previously, `//// foo` and `/*** foo ***/` were accepted as doc comments. This
changes that, so that only `/// foo` and `/** foo ***/` are accepted. This
confuses many newcomers and it seems weird.

Also update the manual for these changes, and modernify the EBNF for comments.

Closes #10638