Search code examples
coqproof-general

what is [...] in proof general and why can't I delete it

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.

Solution

  • 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