Resolve doxycomment duplication debate

I believe putting comments in the headers has won by a good margin, with everyone other than me preferring it, so time to enshrine it.