Consitently use documentation comments (** *) for explanations.

[chdoc]

In order to obtain decently looking documentation, we should consistent in our use of comments and documentation:

• documentation comments (** *) for everything that qualifies as explanation (rendered in highlighted boxes in the documentation).
• regular comments (* *) for TODO and TOTHINK comments and the like, that are internal (rendered as greyed-out text)

(edit: comments inside proofs must always be regular comments, as documentation inside proofs messes up coqdocjs code folding)