Is your feature request related to a problem?

The Diffs option only influences default goal output in rocq top but not the Show command and there is no Show diffs. As a consequence there seems to be no way to highlight differences in the goals when the Silent flag is set. Therefore the diffs option is nonfunctional in the master branch of ProofGeneral when with the default of running rocq silent, see also ProofGeneral/PG#835.

Proposed solution

Please provide a way to highlight differences in the goals the simple Show command that displays the current goals, similarly to Show Proof Diffs. Or change the simple Show command, such that it is affected by the Diffs option.

Alternative solutions

No response

Additional context

No response