diff --git a/CHANGES b/CHANGES index f27719060..8e7720739 100644 --- a/CHANGES +++ b/CHANGES @@ -40,6 +40,10 @@ 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 and Printing Notations can be set/unset + via menu and Coq keymap (C-c C-a C-9 and C-c C-a C-0 for + Parentheses (optimized for British and American keyboards); C-c + C-a n and C-c C-a N for Notations). *** 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..3eefa6054 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -335,6 +335,10 @@ ["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 Notations" coq-set-printing-notations t] + ["Unset Printing Notations" coq-unset-printing-notations 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 4eb493810..2b83a1ddd 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1771,6 +1771,10 @@ 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-notations "Set Printing Notations.") +(proof-definvisible coq-unset-printing-notations "Unset Printing Notations.") (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.") @@ -2861,6 +2865,10 @@ 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) +(define-key coq-keymap [(?N)] #'coq-set-printing-notations) +(define-key coq-keymap [(?n)] #'coq-unset-printing-notations) ;(proof-eval-when-ready-for-assistant ; (define-key ??? [(control c) (control a)] (proof-ass keymap)))