OK for me. Thanks for taking the time to submit this.
If there is no objection I will commit this.
2011/6/3 Erik Martin-Dorel <erik.martin-do...@ens-lyon.fr>:
> Dear all,
> If it is not too late for inclusion in ProofGeneral 4.1, may I suggest
> to apply the enclosed patch for Coq PG bindings?
> More precisely, [C-c C-a C-r] becomes a shortcut for `coq-insert-requires'
> that was not bound to any key (the corresponding line was commented),
> and the four following shortcuts are slightly simplifed:
> [C-c C-a C-S-h]
> [C-c C-a C-S-g]
> [C-c C-a C-S-r]
> [C-c C-a C-S-t]
> [C-c C-a h] for `coq-PrintHint'
> [C-c C-a g] for `proof-store-goals-win'
> [C-c C-a r] for `proof-store-response-win'
> [C-c C-a t] for `coq-insert-tactical'
> These new keys are easier to type, tty-compliant, and do not overwrite
> any other ProofGeneral keys.
> Kind regards,
> Érik Martin-Dorel
> PhD student, ENS de Lyon, LIP
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list