CODEWITHSUNDEEP
coqproof-general
push33n
push33n

Reputation: 477

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.

Upvotes: 2

Views: 178

Answers (1)

ErikMD
ErikMD

Reputation: 14763

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

Upvotes: 3

Related Questions