diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2012-09-25 11:36:43 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2012-09-25 11:36:43 +0000 |
| commit | e45c11ad24987b32b2046f3c2163d07ccf0ccec0 (patch) | |
| tree | c36546044675a29275948d817303034a2893ab1b /coq/coq-abbrev.el | |
| parent | 50fcb507ff60cad600bcaa814230fecc5ef2646f (diff) | |
Fixed #419: coq synchronized variables are not anymore in the settings
menu, they are in option menu that only issues commands to the prover
and do not try to keep track of the values of the variables.
Diffstat (limited to 'coq/coq-abbrev.el')
| -rw-r--r-- | coq/coq-abbrev.el | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 5242b4f1..8f5f6634 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -80,7 +80,7 @@ ;; Common part (scrit, response and goals buffers) (defconst coq-menu-common-entries `( - ["Toggle 3 Windows Mode" proof-three-window-toggle + ["Toggle 3 Windows Mode" proof-three-window-toggle :style toggle :selected proof-three-window-enable :help "Toggles the use of separate windows or frames for Coq responses and goals." @@ -163,7 +163,18 @@ "" ["Locate notation..." coq-LocateNotation t] ["Print Implicit..." coq-Print t] - ["Print Scope/Visibility..." coq-PrintScope t]))) + ["Print Scope/Visibility..." coq-PrintScope t]) + ("OPTIONS" + ["Set Printing All" coq-set-printing-all t] + ["UnSet Printing All" coq-unset-printing-all t] + ["Set Implicit Argument" coq-set-implicit-arguments t] + ["Unset Implicit Argument" coq-unset-implicit-arguments 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] + ["Unset Printing Coercions" coq-unset-printing-coercions t] + ["Set Printing Wildcards" coq-set-printing-wildcards t] + ["Unset Printing Wildcards" coq-unset-printing-wildcards t]))) (defpgdefault menu-entries (append coq-menu-common-entries |