cleanup: coqdoc fixes and unnecessary ideal uniprocessor assumption

Remove the use of ideal uniprocessor schedules in a couple of places where
it's not actually required.

Also fix some coqdoc styling issues while at it.