diffs not shown when Coq is run completely silent

[Flupp]

When coq-run-completely-silent is enabled, then coq-diffs has no effect and diffs are never shown.

When diffs are needed, coq-run-completely-silent can be disabled as a workaround.

When coq-run-completely-silent is enabled, Proof General requests goals explicitly via Show command, however, the output is then without diff markup. The Show Proof command (which displays the proof term; not the goal) has optional parameters for enabling printing with diff. There does not seem to be an equivalent for demanding a diff when explicitly showing goals.

[hendriktews]

See rocq-prover/rocq#20793; @Matafou @erikmd @cpitclaudel : maybe you are interested in leaving a comment in this rocq issue?