M-. failure

[vzaliva]

Pressing M-. on definition fails with error "company-coq--get-comment-region: Symbol’s function definition is void: coq-find-comment-start"

[Isweet]

I'm also getting this error.

OSX Version 10.14.6
Emacs Version 26.2
Coq Version 8.9.1
Proof General Version 20190821.848
Company-Coq Version 20190425.1851

[vzaliva]

It started happening again

[cpitclaudel]

OK, I'll take a look at getting a better fix this week-end

[vzaliva]

thanks! It is really annoyng bug as it is very common functionality used often.

[vzaliva]

I did some additional digging, and functions coq-find-comment-start and coq-find-comment-end are commented out in current MELPA version (20191007.1041) of proof general's coq-indent.el ( https://github.com/ProofGeneral/PG/blob/master/coq/coq-indent.el#L284 ).

[vzaliva]

Currently, this works, fixed by ProofGeneral/PG#444
However, they had a suggestion:

Probably a better option is to fix company-coq so it uses
syntax-ppss and forward-comment instead. E.g.

    (let ((ppss (syntax-ppss))) (when (nth 4 ppss) (nth 8 ppss))))

will return the position of the beginning of the comment if you're
inside a comment or nil otherwise. And (forward-comment 1) will jump
from the beginning of a comment to its end.

I leave this issue open for now. If you do not plan to implement this suggestion and happy with current mechanism, feel free to close it.