diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-03-13 14:11:31 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-03-13 14:11:31 +0000 |
| commit | ee094de6145730aad0774adf9ac9f931a1b07cf0 (patch) | |
| tree | fd2cec612a431bb7a6fcec882789875e20438c7f /coq/coq-abbrev.el | |
| parent | d3db21f910d8e4efa8d88de02371bac855500b8b (diff) | |
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.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 2ccf5cab..431f463f 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -132,6 +132,7 @@ ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"] + ["Other..." coq-query] [ "Store Response" proof-store-response-win :help "Stores the content of response buffer in a dedicated buffer"] [ "Store Goal" proof-store-goals-win :help "Stores the content of goals buffer in a dedicated buffer"] ("OTHER QUERIES" |