aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-abbrev.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-12 20:49:05 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-12 20:49:05 +0200
commit14b8d0e24ef48032885018b4020969593477ee26 (patch)
tree9e9b6d76aee7fc03659cf5149e8a5039129818bf /coq/coq-abbrev.el
parent6effc3a06b96a791805d69c7dd82ef59349abf26 (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 'coq/coq-abbrev.el')
-rw-r--r--coq/coq-abbrev.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index a088fba8..e664317f 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -172,7 +172,7 @@
["UnSet Printing All" coq-unset-printing-all t]
["Set Implicit Argument" coq-set-implicit-arguments t]
["Unset Implicit Argument" coq-unset-implicit-arguments t]
- ["Adapt Printing Width" coq-adapt-printing-width t]
+ ["Set Printing Width" coq-ask-adapt-printing-width-and-show t]
["Set Printing Synth" coq-set-printing-synth t]
["Unset Printing Synth" coq-unset-printing-synth t]
["Set Printing Coercions" coq-set-printing-coercions t]