Rename .dox files to end with .md, and remove their /** magic **/

I thought that we had to have documentation-only doxygen files wrapped in /** and **/. But we don't: we can just tell doxygen that those files are markdown, and it will do the right thing.

We should make this change so that other tools (like github) that have special handling for markdown can pretty-print our markdown files, and so that we can eventually incorporate some/all of doc/HACKING into our doxygen.