Coq: make printing parentheses flag accessible

Add menu entry and Coq keymap binding available to set/unset the
Printing Parentheses flag.

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

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]

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)))