Merge PR #10494: Show diffs in "Show Proof."

Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin

2 files changed, 18 insertions, 3 deletions

diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
new file mode 100644
index 0000000000..c1df728c5c
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst
@@ -0,0 +1,6 @@
+- Optionally highlight the differences between successive proof steps in the
+  :cmd:`Show Proof` command.  Experimental; only available in coqtop
+  and Proof General for now, may be supported in other IDEs
+  in the future.
+  (`#10494 <https://github.com/coq/coq/pull/10494>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 57a54bc0ad..00f8269dc3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -535,7 +535,7 @@ Requesting information
             eexists ?[n].
             Show n.
 
-   .. cmdv:: Show Proof
+   .. cmdv:: Show Proof {? Diffs {? removed } }
       :name: Show Proof
 
       Displays the proof term generated by the tactics
@@ -544,6 +544,12 @@ Requesting information
       constructed. Each hole is an existential variable, which appears as a
       question mark followed by an identifier.
 
+      Experimental: Specifying “Diffs” highlights the difference between the
+      current and previous proof step.  By default, the command shows the
+      output once with additions highlighted.  Including “removed” shows
+      the output twice: once showing removals and once showing additions.
+      It does not examine the :opt:`Diffs` option.  See :ref:`showing_diffs`.
+
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
 
@@ -624,8 +630,11 @@ Showing differences between proof steps
 ---------------------------------------
 
 
-Coq can automatically highlight the differences between successive proof steps and between
-values in some error messages.
+Coq can automatically highlight the differences between successive proof steps
+and between values in some error messages.  Also, as an experimental feature,
+Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof`
+command, but only, for now, when using coqtop and Proof General.
+
 For example, the following screenshots of CoqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added