diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-12 20:49:05 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-12 20:49:05 +0200 |
| commit | 14b8d0e24ef48032885018b4020969593477ee26 (patch) | |
| tree | 9e9b6d76aee7fc03659cf5149e8a5039129818bf /CHANGES | |
| parent | 6effc3a06b96a791805d69c7dd82ef59349abf26 (diff) | |
proof-assert-command-hook added + Auto adjust width in coq mode.
This hook was missing, it allows to send complete commands before
the (set of) command(s) sent by the user. It shall be used when
proof-shell-insert-hook cannot be used (because of multiple prompts
appearing).
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 11 |
1 files changed, 8 insertions, 3 deletions
@@ -122,13 +122,18 @@ 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. -*** Set Printing Width adapted to goals window size +*** Auto adjusting of printing width - (coq-adapt-printing-width) sets the coq printing width to the - width of goals window. Default binding: C-c C-a C-w. + On by default. To disable: Coq/Settings/Auto Adapt Printing Width. *** Coq Querying facilities +*** Removed the Set Undo 500 at start. + This is obsolete. To recover: (setq coq-user-init-cmd `("Set Undo 500.")) + + + + **** Minibuffer interactive queries Menu Coq/Other Queries (C-c C-a C-q) allows to send queries (like |