Search code examples
emacscoqproof-general

Remove arrow in Emacs' ProofGeneral mode for Coq

I'm using ProofGeneral with Coq. When I do C-c C-return, Emacs highlights the area Coq has processed. This is nice. However, it inserts a '=>' on the next line, which overwrites the first two characters of your input. For example, currently I'm looking at

Inductive Seq : Set :=
| MkSeq : Ants -> Form -> Seq.

=>ductive Prf : Set :=
| Init :

How can I get rid of that arrow?

Update:

I learned that if I turn fringe-mode on, the arrow is in the fringe and I can see all my typing. I still want to kill it though. Thanks!

Solution

  • Aha, just found it. This is an Emacs configuration, not a Proof General one, given in the overlay-arrow-string variable. To turn it off, just set the variable to "" in your Emacs configuration puttng this in your .emacs:

    (setq overlay-arrow-string "")