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 <[email protected]>: > 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 > [email protected] > http://perso.ens-lyon.fr/erik.martin-dorel/ > > _______________________________________________ > ProofGeneral-devel mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > > _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
