2

I am using proof-general mode for editing and executing Coq files in emacs. However, I am highly annoyed by the C-c C-n behavior of always going to the next line if the EoF is reached. As I tend to use it interactively, executing the proof as I go along I end up always typing: C-c C-n + ARROW-UP + END.

How can I change that behavior of C-c C-n to ONLY evaluate to the next dot? Alternative: Is there a command I overlooked that does exactly that?

Gilles 'SO- stop being evil'
  • 21,702
  • 4
  • 53
  • 89
Sim
  • 123
  • 5

1 Answers1

1

As a way around it I'm having extra commands written on the line, so that end-of-line isn't reached after executing C-c C-n: Proof. .. That extra dot ensures that when Proof. is executed the cursor still stays on the same line.

Slavik Derevianko
  • 126
  • 2