From 7501326a228a5d0af1ad1d5bef4e8640cbd1e43f Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 15 May 2019 13:08:02 -0700
Subject: Do a "Set Diffs" whenever backtracking.  This also re-prints the
 context (with diff annotations when enabled).

---
 coq/coq.el            | 3 ++-
 doc/ProofGeneral.texi | 6 +++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 67abb4f6..21b1acf9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1216,7 +1216,8 @@ be called and no command will be sent to Coq."
           (> (length (coq-get-span-proofstack (proof-last-locked-span)))
              ;; the number of aborts is the third arg of Backtrack.
              (string-to-number (match-string 1 cmd)))))
-    (list "Unset Silent." "Show."))
+    ; "Set Diffs" always re-prints the proof context with (if enabled) diffs
+    (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
      ;; silent (there is no goal to show).
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 73bb98e5..ec449cc0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -5226,9 +5226,9 @@ select @code{Coq -> Settings -> Save Settings}.
 
 The colors used to highlight diffs are configurable in the
 @code{Proof-General -> Advanced -> Customize -> Proof Faces} menu.
-The 4 @code{Coq Diffs ...} faces control the highlights.  Any line that
-has added or removed tokens are shown with the entire line highlighted with
-a @code{Bg} face.  The added or removed tokens themselves are highlighted
+The 4 @code{Coq Diffs ...} faces control the highlights.  Lines that
+have added or removed tokens are shown with the entire line highlighted with
+a @code{Coq Diffs ... Bg} face.  The added or removed tokens themselves are highlighted
 with non-@code{Bg} faces.
 
 @c =================================================================
-- 
cgit v1.2.3