From 5ade280786a6eb85c6b533cdf82cf9aafef1c8c5 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 24 Jul 2012 09:27:16 +0000
Subject: Fixing compilation. Still need to verify some smie stuff on different
 versions of emacs.

---
 CHANGES | 35 ++++++++++++++++++++++++++---------
 1 file changed, 26 insertions(+), 9 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index d9b7dce8..b842ccf3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,10 +29,32 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
 
 *** Support proof-tree visualization
 
-*** Indentation improvements using SMIE
-    Still experimental.
+*** New commands for Print/Check/About/Show with "Printing All" flag
+    Avoids typing "Printing All" in the buffer. See the menu Coq >
+    Other queries. Thanks to Assia Mahboubi and Frederic Chyzak for
+    the suggestion.
+    Shortcut: add C-u before the usual shortcut
+     (example: C-u C-c C-a C-c for:
+     	        Set Printing All.
+		Check.
+		Unset Printing All. )
+
+*** Coq menu visible in Response and goals buffers.
+    Shortcuts available too (Check, Print etc.) in response and goals
+    buffers.
+
+*** Tooltips hidden by default
+    Flickering when hovering commands is off by default!
 
-****  Limitations:
+*** "Insert Requires" now uses completion based on coq-load-path
+
+*** New setting for hiding additional goals from the *goals* buffer
+    Coq > Settings > Hide additional subgoals
+
+*** Indentation improvements using SMIE. Supporting bullets and { }.
+    Still experimental. Please submit bugs.
+
+****  Limitations of indentation:
 
 ***** hard-wired precedence between bullets: - < + < *
      example:
@@ -51,12 +73,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
       always introduce a proof with "Proof." (or "Next Obligation").
 
 *** Minor parsing fixes
-
-*** New setting for hiding additional goals from the *goals* buffer
-
-*** New commands for Print/Check/Show with Printing All flag
-
-*** "Insert Requires" now uses completion based on coq-load-path
+*** Windows resizing fixed
 
 ** HOL Light  [WORK IN PROGRESS]
 
-- 
cgit v1.2.3