Improve (company-coq-occur) to cope with non-one-liner statements?

[erikmd]

Dear @cpitclaudel,

@pPomCo and I like the (company-coq-occur) function very much (bound to C-c C-,)

but it often happens that definitions and lemmas are not one-liners… so that we end up with non-informative truncated statements (only the first line :-/)

Do you think it would be easy to extend (company-coq-occur) so that C-c C-, or C-u C-c C-, (for example) includes the whole definition/statement upto the next .<whitespace>?

In any case, let us know if you'd be ready to accept a PR to this aim.

[cpitclaudel]

Yes, I'd love to merge a PR for that. But doesn't company-coq-fold do what you want/need?

[erikmd]

Hi @cpitclaudel, OK!

But doesn't company-coq-fold do what you want/need?

We weren't aware of this one… it indeed helps for our use case, thanks :)