diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2012-07-09 22:26:02 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2012-07-09 22:26:02 +0000 |
| commit | 0c32a39131f62ff1b19f4395d28c057b64074eb6 (patch) | |
| tree | 70b845d46d5bc0012c5d841de6bcc02ac3a00d13 /coq/coq-abbrev.el | |
| parent | 1859db80d88a5abd7dba87e686916347c5f57415 (diff) | |
Added completion to insert Require, based on coq-load-path.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index c279e91b..bc194d74 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -20,7 +20,7 @@ (defconst coq-tactics-menu (append '("Tactics (menu)" - ["Intros (smart)" coq-insert-intros t]) + ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]) (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db)))) (defconst coq-tactics-abbrev-table @@ -80,6 +80,10 @@ (defpgdefault menu-entries `( ["Toggle 3 windows mode" proof-three-window-toggle t] + ["Toggle tooltips" proof-output-tooltips-toggle + :style toggle + :selected proof-output-tooltips + :help "Toggles tooltips (popup when hovering commands).\nSet `proof-output-tooltips' to nil to disable it by default."] "" ["Print..." coq-Print t] ["Check..." coq-Check t] @@ -118,16 +122,16 @@ ) "" ("INSERT" + ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."] "" ["tactic (interactive)" coq-insert-tactic t] - ,coq-tactics-menu ["tactical (interactive)" coq-insert-tactical t] - ,coq-tacticals-menu - "" ["command (interactive)" coq-insert-command t] - ,coq-commands-menu - "" ["term (interactive)" coq-insert-term t] + "" + ,coq-tactics-menu + ,coq-tacticals-menu + ,coq-commands-menu ,coq-terms-menu "" ["Module/Section (smart)" coq-insert-section-or-module t] |