Suggestion to recover the default C-h suffix for Emacs keys help

[Erik Martin-Dorel]

The commands [C-c C-h] and [C-c C-a C-h] are currently assigned to the ProofGeneral commands proof-help and coq-PrintHint.

The drawkback of these key bindings is that they overwrite the default "C-h suffix" provided by Emacs, which allows to get a list of shorcuts that start with a given prefix key (as with [C-x 4 C-h] for instance).

To recover this convenient feature in ProofGeneral, I would suggest to do the following slight changes:

In generic/proof-menu.el, assign proof-help to

(define-key map [(control c) (control H)] 'proof-help)

and in coq/coq.el, assign coq-PrintHint to

(define-key coq-keymap [(control ?H)] 'coq-PrintHint)

as these new bindings with capital H are free, and will be reminded to the user by Emacs if ever he tried the legacy shorcuts with small h.

Kind Regards, Erik Martin-Dorel.

[David Aspinall]

Erik: many thanks for the excellent suggestion (and reminder of that feature); implemented as proposed.