From 6dabc28114f0ee2ba03b79c4bdd313154cab8d30 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 9 Sep 2010 16:58:33 +0000
Subject: Fixed the cleaning of goals buffer when proof completed + fixed the
 refreshing of modeline goal number display.

---
 CHANGES | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 5b35b7ed..37d3b4db 100644
--- a/CHANGES
+++ b/CHANGES
@@ -97,11 +97,14 @@
     persistent buffer (for later use), use Coq/Store response or
     Coq/Store goal.
 
-*** bug fixes
+*** bug fixes, bugs
     - Three panes mode: "window would be too small" error fixed.
     - Indentation: several error fixed. If you want to indent tactics
     inside "Instance" or "Add Parametric Relation" etc, please put
-    "Proof." before the tactics.
+    "Proof." before the tactics, there is no way for emacs to guess
+    wether these commands initiate new goals or not.
+    - coq prog args permanent settings is working again
+    - when a proof is completed, the goals buffer is cleared again.
 
 ** Notable internal changes
 
-- 
cgit v1.2.3