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

Reply via email to