From ee094de6145730aad0774adf9ac9f931a1b07cf0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Fri, 13 Mar 2015 14:11:31 +0000
Subject: Added a command to send Queries to coq, with completion (C-c C-a
 C-q).

Should replace C-c C-v at some point. Needs to have a complete list of
such queries. Obeys C-u prefix for Printing all flag.
---
 CHANGES | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 4d7b23d5..d09b67cb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -116,7 +116,20 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
     Experimental: colorize hypothesis names and some parts of error
     and warning messages. For readability.
 
-*** mouse Queries
+*** Coq Querying facilities
+
+**** Minibuffer interactive queries
+
+    Menu Coq/Other Queries (C-c C-a C-q) allows to send queries (like
+    Print, Locate...) (à la auctex) without inserting them in the
+    buffer. Queries are TAB completed and the usual history mechanism
+    applies. Completion allows only a set of state preserving
+    commands. The list is not exhaustive yet.
+
+    This should replace the C-c C-v usual command mechanism (which has
+    no completion).
+
+**** Mouse Queries
 
     This remaps standard emacs key bindings (faces and buffers menus
     popup), so this is not enabled by default, use (setq
@@ -128,7 +141,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
       that id.
 
     As most of the bindings, they are active in the three buffer
-    (script, goals, response).
+    (script, goals, response). Obeys C-u prefix for "Printing all"
+    flag.
 
 *** bug fixes
     - Annoying cursor jump when hitting ".".
-- 
cgit v1.2.3