From e45c11ad24987b32b2046f3c2163d07ccf0ccec0 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 25 Sep 2012 11:36:43 +0000 Subject: 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. --- coq/coq-abbrev.el | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'coq/coq-abbrev.el') 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 -- cgit v1.2.3