Is there anybody working on this for the RC? If so it needs an assignee.

@BastienSozeau and @mattam82: what is the status? Note that it would be really preferable to have this completed in the rc, which is going to be released next week.

Here you can see (temporarily) the proposed changes to the refman

https://rocq-prover.org/doc/master/refman/proofs/writing-proofs/proof-mode.html

@BastienSozeau shouldn't the Rocq code examples be different as well as you modified the coqdoc style?

The proposed theme mostly looks good to me, except for the orange background of the top-left corner. I would prefer using the blue and having the text in white as before. Or use a lighter orange there. I like the light orange of the tactics / commands.