9 files changed, 125 insertions, 5 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
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index f6fca91eea..a806ab7123 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -16,6 +16,9 @@ val write_diffs_option : string -> unit
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
+(** Returns true if the diffs option is "removed" *)
+val show_removed : unit -> bool
+
 (** controls whether color output is enabled *)
 val write_color_enabled : bool -> unit
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 413c6540a3..47bb0a6af0 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -55,8 +55,7 @@ let get_current_goal_context pf =
     let env = Global.env () in
     Evd.from_env env, env
 
-let get_current_context pf =
-  let p = Proof_global.get_proof pf in
+let get_proof_context p =
   try get_goal_context_gen p 1
   with
   | NoSuchGoal ->
@@ -64,6 +63,10 @@ let get_current_context pf =
     let { Proof.sigma } = Proof.data p in
     sigma, Global.env ()
 
+let get_current_context pf =
+  let p = Proof_global.get_proof pf in
+  get_proof_context p
+
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index 30514191fa..11ce50b659 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env
 (** [get_current_goal_context ()] works as [get_goal_context 1] *)
 val get_current_goal_context : Proof_global.t -> Evd.evar_map * env
 
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_context : Proof.t -> Evd.evar_map * env
+
 (** [get_current_context ()] returns the context of the
   current focused goal. If there is no focused goal but there
   is a proof in progress, it returns the corresponding evar_map.
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
new file mode 100644
index 0000000000..285a3bcd89
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -0,0 +1,42 @@
+
+Coq < Coq < 1 subgoal
+  
+  ============================
+  [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x < 
+x < 1 focused subgoal
+(shelved: 1)
+  [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+  ============================
+  [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m?j[49m
+   [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+      [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x < 
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v
new file mode 100644
index 0000000000..4251c52cb4
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.v
@@ -0,0 +1,6 @@
+(* coq-prog-args: ("-color" "on" "-diffs" "on") *)
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.  Show Proof Diffs.
+  eexists.  Show Proof Diffs.
+  split.  Show Proof Diffs.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 1f319d2bfd..97f0e57d2e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -418,6 +418,50 @@ let rec vernac_loop ~state =
       Feedback.msg_notice (v 0 (goal ++ evars));
       vernac_loop ~state
 
+    | Some VernacShowProofDiffs removed ->
+      (* extension of Vernacentries.show_proof *)
+      let to_pp pstate =
+        let p = Option.get pstate in
+        let sigma, env = Pfedit.get_proof_context p in
+        let pprf = Proof.partial_proof p in
+        Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
+        (* We print nothing if there are no goals left *)
+      in
+
+      if not (Proof_diffs.color_enabled ()) then
+        CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
+      else begin
+        let out =
+          try
+            let n_pp = to_pp state.proof in
+            if true (*Proof_diffs.show_diffs ()*) then
+              let doc = state.doc in
+              let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
+              try
+                let o_pp = to_pp oproof in
+                let tokenize_string = Proof_diffs.tokenize_string in
+                let show_removed = Some removed in
+                Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
+              with
+              | Pfedit.NoSuchGoal
+              | Option.IsNone -> n_pp
+              | Pp_diff.Diff_Failure msg -> begin
+                (* todo: print the unparsable string (if we know it) *)
+                Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
+                    ++ str "Showing results without diff highlighting" );
+                n_pp
+                end
+            else
+              n_pp
+          with
+          | Pfedit.NoSuchGoal
+          | Option.IsNone ->
+            CErrors.user_err (str "No goals to show.")
+        in
+        Feedback.msg_notice out;
+      end;
+      vernac_loop ~state
+
     | None ->
       top_stderr (fnl ()); exit 0
 
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index e180d9e750..56fda58a25 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -22,6 +22,7 @@ type vernac_toplevel =
   | VernacQuit
   | VernacControl of vernac_control
   | VernacShowGoal of { gid : int; sid: int }
+  | VernacShowProofDiffs of bool
 
 module Toplevel_ : sig
   val vernac_toplevel : vernac_toplevel option Entry.t
@@ -59,6 +60,8 @@ GRAMMAR EXTEND Gram
       (* show a goal for the specified proof state *)
       | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
           { Some (VernacShowGoal {gid; sid}) }
+      | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." ->
+        { Some (VernacShowProofDiffs (removed <> None)) }
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None