doc/other.xml: Some DocBook markup changes.