刪除Emacs的ProofGeneral模式中的箭頭Coq

我正在使用ProqGeneral和Coq。當我進行C-C C返回時，Emacs會突出顯示Coq已處理的區域。這很好。但是，它在下一行插入'=>'，它會覆蓋輸入的前兩個字符。例如，目前我在看刪除Emacs的ProofGeneral模式中的箭頭Coq

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

=>ductive Prf : Set := 
| Init :

我該如何擺脫那個箭頭？

更新：

我知道，如果我把劉海模式上，箭頭在邊緣，我可以看到我的所有打字。我仍然想要殺死它。謝謝！

2013-10-18 seanmcl

你有這個問題在圖形模式下運行的Emacs是什麼時候？你使用的是哪個版本的Emacs和PG？ –

是的，圖形模式。最新的PG，Emacs 24.2。就像我說的那樣，只有當我有邊緣模式關閉時。但是我沒有找到與邊緣模式有關的PG源中的任何東西。 – seanmcl

啊哈，剛剛找到它。這是一個Emacs配置，而不是overlay-arrow-string變量中給出的證明通用配置。要關閉它，只需設置變量""在您的Emacs配置puttng這在.emacs：

(setq overlay-arrow-string "")

2013-10-18 20:22:09

謝謝！當我回家時，我會給你點分數，當它工作:) – seanmcl

回答