When I try and copy paste proof code, sometimes a [...] will show up (even though I did not copy anything of the kind) and I cannot delete it. I have to undo the copy in order to get rid of it. What does this mean?
Thanks.
As confirmed in the comments, the occurrences of […] correspond here to the code folding feature of company-coq.
To toggle the visibility of a block (starting with a brace, e.g.
Goal True /\ True.
split.
{ […]
or starting with a bullet, e.g.
Goal True /\ True.
split.
- idtac. […]
), you can just move the point to the opening symbol { or -, and press RET
Otherwise, to "unfold" all blocks of the ambient buffer, you can do:
M-x company-coq-features/code-folding-reset-to-initial-state RET