From 9b41ff4e90a0303d9caf6e7e2f951a5046ce2d13 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 28 Apr 2019 12:04:54 -0700
Subject: Highlight diffs in goals and some error messages using Coq's proof
 diffs feature.

---
 CHANGES | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 02da6c87..4195c26a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,7 +75,6 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
    
    Hide/ unhide status remains when goal changes.
 
-
 *** Highlighting of hypothesis
 
     You can highlight hypothesis in goals buffer on a per name
@@ -84,8 +83,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
 
     Highlighting status remains when goal changes.
 
-
-**** Automtic highlighting with (search)About.
+**** Automatic highlighting with (search)About.
     Hypothesis cited in the response buffer after C-c C-a C-a (i.e.
     M-x coq-SearchAbout) will be highlighted automatically. Any other
     hypothesis highlighted is unhighlighted.
@@ -94,6 +92,10 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
 
     (setq coq-highlight-hyps-cited-in-response nil)
 
+*** Support Coq's feature for highlighting the differences
+    between successive proof steps.  See section 11.8 ("Showing
+    Proof Diffs") in the documentation.
+
 *** bug fixes
     - avoid leaving partial files behind when compilation fails
     - 123: Parallel background compliation fails to execute some
-- 
cgit v1.2.3