diff --git a/CHANGES b/CHANGES index f27719060..52ae7c939 100644 --- a/CHANGES +++ b/CHANGES @@ -40,6 +40,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG *** New command `proof-check-annotate' to annotate all failing proofs with FAIL comments. Useful in the development process as described above to ensure all currently failing proofs are marked as such. +*** flag Printing Parentheses can be set/unset via menu + and Coq keymap (C-c C-a C-9 and C-c C-a C-0, optimized for British + and American keyboards) *** New options coq-compile-extra-coqc-arguments and coq-compile-extra-coqdep-arguments to configure additional command line arguments to calls of, respetively, coqc and coqdep diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 14658c51e..486fde0e8 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -335,6 +335,8 @@ ["Unset Printing All" coq-unset-printing-all t] ["Set Printing Implicit" coq-set-printing-implicit t] ["Unset Printing Implicit" coq-unset-printing-implicit t] + ["Set Printing Parentheses" coq-set-printing-parentheses t] + ["Unset Printing Parentheses" coq-unset-printing-parentheses t] ["Set Printing Coercions" coq-set-printing-coercions t] ["Unset Printing Coercions" coq-unset-printing-coercions t] ["Set Printing Compact Contexts" coq-set-printing-implicit t] diff --git a/coq/coq.el b/coq/coq.el index 9d23dafca..61c760793 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1775,6 +1775,8 @@ See `coq-fold-hyp'." (proof-definvisible coq-unset-printing-implicit "Unset Printing Implicit.") (proof-definvisible coq-set-printing-all "Set Printing All.") (proof-definvisible coq-unset-printing-all "Unset Printing All.") +(proof-definvisible coq-set-printing-parentheses "Set Printing Parentheses.") +(proof-definvisible coq-unset-printing-parentheses "Unset Printing Parentheses.") (proof-definvisible coq-set-printing-synth "Set Printing Synth.") (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.") (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.") @@ -2862,6 +2864,8 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [(control ?l)] #'coq-LocateConstant) (define-key coq-keymap [(control ?n)] #'coq-LocateNotation) (define-key coq-keymap [(control ?w)] #'coq-ask-adapt-printing-width-and-show) +(define-key coq-keymap [(control ?9)] #'coq-set-printing-parentheses) +(define-key coq-keymap [(control ?0)] #'coq-unset-printing-parentheses) ;(proof-eval-when-ready-for-assistant ; (define-key ??? [(control c) (control a)] (proof-ass keymap)))