OK for me. Thanks for taking the time to submit this.
If there is no objection I will commit this.
P.C.

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]
> become:
> [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,
>
> Erik
>
> --
> √Črik Martin-Dorel
> PhD student, ENS de Lyon, LIP
> erik.martin-do...@ens-lyon.org
> http://perso.ens-lyon.fr/erik.martin-dorel/
>
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to