The Coq mailing list

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

Thomas Braibant 
<thomas.braibant AT gmail.com>
 writes:

   > Use electric terminator? I hate it but it will save you typing some "go
   > forward" commands.

I always use the electric terminator. But I have bound
proof-undo-last-successful-command (C-c C-u) to just one key,
such that I can quickly undo its effect.

   BTW, when doing go forward at the end of a line that ends
   with a period, pg moves the cursor to the next line, which is most
   often not what I want it to do

If you have problems like this please do raise them on coq-club,
ProofGeneral-devel, open an issue in the Proof General tracker or
file a Debian bug report. Often there are simple solutions.

   Which makes we wonder: as (the/a?) developer of the PG Coq mode, have
   you thought about gathering statistics about what kind of commands
   people use, and which one are never used? 

I believe the missing feedback from Coq Proof General users is
generally a problem for the Proof General developers. For
instance, the new automatic library compilation of Proof General
works great for me. But I have no idea what non-Proof-General
developers think about it.


Bye,

Hendrik