Show diffs in "Show Proof."

Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output

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