The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

   - find an emacs way to exchange _ and - in my keyboard layout (a
   particular instance of the following point)

I would use xmodmap to switch keys, to ensure that you have the
changed layout in all applications. 

   - find a way to shorten the number of key presses required to write
   proof scripts

I insert many tactics with just two keys presses. For instance 
"` o" inserts "omega.",  "` s" inserts "simpl." and so on. For more
complex tactics I query arguments from the minibuffer, eg. "` m"
inserts "decompose [ex and or] H; clear H.", where the assumption
H is queried in the minibuffer.

The idea is borrowed from Pvs: some rarely used key (`) is made a
prefix key in Emacs, such that you can bind commands to key
sequences starting with `.


For copying bigger amounts of text, especially for generalize, I
use the virtual cursor of package vcursor.el. With it you can
navigate a second cursor in the goals buffer and then copy text
from there to the proof script without touching the mouse or
loosing your real cursor position.

Bye,

Hendrik