[…]在一般情况下是什么，为什么我不能删除它

Question

[当我尝试复制粘贴证明代码时，有时会显示[...]（即使我没有复制任何形式的东西），也无法删除它。我必须撤消该副本才能摆脱它。这是什么意思？

谢谢。

Answer 1

如评论中所确认，[…]的出现在此对应于code folding feature的company-coq。

[切换块的可见性（例如，以大括号开头

Goal True /\ True.
split.
{ […]

或以子弹开头，例如

Goal True /\ True.
split.
- idtac. […]

），只需将点移动到开始符号{或-，然后按RET

否则，要“展开”环境缓冲区的所有块，可以执行：

M-x << [company-coq-features / code-folding-reset-to-initial-state RET