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/
Index: coq/coq.el =================================================================== RCS file: /disk/cvs/proofgen/ProofGeneral/coq/coq.el,v retrieving revision 11.37 diff -c -r11.37 coq.el *** coq/coq.el 25 May 2011 07:23:04 -0000 11.37 --- coq/coq.el 2 Jun 2011 21:53:33 -0000 *************** *** 1899,1923 **** (define-key coq-keymap [(control ?))] 'coq-end-Section) (define-key coq-keymap [(control ?s)] 'coq-Show) (define-key coq-keymap [(control ?t)] 'coq-insert-tactic) ! (define-key coq-keymap [(control ?T)] 'coq-insert-tactical) ! (define-key coq-keymap [(control ?r)] 'proof-store-response-win) ! (define-key coq-keymap [(control ?G)] 'proof-store-goals-win) - ;(define-key coq-keymap [(control ?!)] 'coq-insert-solve-tactic) (define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty (define-key coq-keymap [(control ?\s)] 'coq-insert-term) (define-key coq-keymap [(control return)] 'coq-insert-command) ! ;(define-key coq-keymap [(control ?)] 'coq-insert-requires) (define-key coq-keymap [(control ?o)] 'coq-SearchIsos) (define-key coq-keymap [(control ?p)] 'coq-Print) (define-key coq-keymap [(control ?b)] 'coq-About) (define-key coq-keymap [(control ?a)] 'coq-SearchAbout) (define-key coq-keymap [(control ?c)] 'coq-Check) ! (define-key coq-keymap [(control ?H)] 'coq-PrintHint) (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) (define-key coq-keymap [(control ?n)] 'coq-LocateNotation) --- 1899,1922 ---- (define-key coq-keymap [(control ?))] 'coq-end-Section) (define-key coq-keymap [(control ?s)] 'coq-Show) (define-key coq-keymap [(control ?t)] 'coq-insert-tactic) ! (define-key coq-keymap [?t] 'coq-insert-tactical) ! (define-key coq-keymap [?r] 'proof-store-response-win) ! (define-key coq-keymap [?g] 'proof-store-goals-win) (define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty (define-key coq-keymap [(control ?\s)] 'coq-insert-term) (define-key coq-keymap [(control return)] 'coq-insert-command) ! (define-key coq-keymap [(control ?r)] 'coq-insert-requires) (define-key coq-keymap [(control ?o)] 'coq-SearchIsos) (define-key coq-keymap [(control ?p)] 'coq-Print) (define-key coq-keymap [(control ?b)] 'coq-About) (define-key coq-keymap [(control ?a)] 'coq-SearchAbout) (define-key coq-keymap [(control ?c)] 'coq-Check) ! (define-key coq-keymap [?h] 'coq-PrintHint) (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) (define-key coq-keymap [(control ?n)] 'coq-LocateNotation)
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
