emacs - 删除 Emacs 的 Coq ProofGeneral 模式中的箭头

Question

我在 Coq 中使用 ProofGeneral。当我执行 Cc C-return 时，Emacs 会突出显示 Coq 已处理的区域。这很好。但是，它会在下一行插入一个“=>”，这会覆盖输入的前两个字符。例如，目前我正在看

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

=>ductive Prf : Set :=
| Init :

我怎样才能摆脱那个箭头？

更新：

我了解到，如果我打开边缘模式，箭头就在边缘，我可以看到我所有的打字。不过我还是想杀了它。谢谢！

Answer 1

啊哈，刚找到。这是overlay-arrow-string变量中给出的 Emacs 配置，而不是 Proof General 配置。要关闭它，只需""在 Emacs 配置中将变量设置为.emacs：

(setq overlay-arrow-string "")